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 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