Recent searches
Search options
I've been learning Lean3 recently, and I'm not sure whether this is just a matter of familiarity, but does it seem significantly more "write-only" compared to pen-and-paper proofs?
I suspect just reading #Lean files is difficult, but maybe if there's an environment displayed on the side, like on the Number Theory Game, it's much easier to reason about the current state of the proof?
@zkproofs Yeah, tactics proofs are very write only for me. I guess you can kind of "embrace it", since you just need to be able to read the definition right, since you're confident the theorem is actually true.
@zkproofs I guess, an automated proof is not a substitute for explanation. (Nor is a pen and paper proof I guess)
@cronokirby yeah, though IME pen-and-paper poofs tend to have more redundancy built-in, which makes understanding easier.
@zkproofs you are 100% supposed to read Lean with a vscode extension/eMacs mode that shows the state on the right. If you’re not doing that, then yeah it’s gonna be a bit hard to follow
@zornsllama heh yeah I was trying to read Lean code on GitHub and wasn’t making it very far lol
@zkproofs yeah tbh don’t even try to do that