https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
I loved it and have been trying to make some subsequent levels about divisibility.
I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels.
Instead, it was so low level that you had to do every step of algebra manually with a line of code each. (and to be fair, in the beginning it was necessary because you're developing the usual rules of algebra as you go, but even in the later levels after they tell you about the ring tactic there's still a lot of manual algebra you need to do) The search space seems small enough that even I was just mindlessly spamming rewrite/intro/apply/induction. Why can't a computer automate this completely.
And going in the other direction, I was hoping this would be a good tool to aid in proofwriting. But most of the "proof" I wrote was complete gibberish not meant for human consumption. I think the problem is because the code relies heavily on mutating a context that you can't see without using the lean UI.
Anyway, maybe the number game is just not a good intro to the full capabilities of lean and I am missing the point.
Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof.
[0] https://www.microsoft.com/en-us/research/publication/write-2...
But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too).
I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)
I too felt it a waste of time to prove things that were clearly "obvious". Of course, in math, some of the most frightening words to encounter are "obvious" and "trivial" but in this case it really was trivial, at the level of proving `a + b = b + a` while working with integers. Tactics like auto, tauto, ring and field help here and should be given more and earlier emphasis in teaching materials. Tactics like `auto` perform like the proof search you mention and others like ring and field make cleverer use of structure.
To fill in the rest of the gap, a project like the Lean math library goes a long way. Not having to provide your own implementation of reals, differential forms or vectors over reals or complex numbers is incredibly useful. I was surprised by how difficult it was to find (I never did) a well maintained and documented library of basic common mathematical structures in Coq.
The second major issue is Formal proofs without their contexts (something like a debugger variables watch list in regular type code), are incomprehensible to most. However, a project, https://plv.csail.mit.edu/blog/alectryon.html, for Literate Formal proofs fully addressed that pain point for me. It's curious how the problem of tedium has a clear path to solution in the Lean community and the equally important flaw of write only proofs is being addressed within the Coq community.
Returning to the issue of what is obvious, a vast amount of mathematical knowledge is tacit, buried in the minds of the respective communities of pure mathematicians. For everyone else, especially users who cannot themselves provide proofs, mathematical knowledge is very often like a Potemkin village. Superficial and artifice, understanding that falls apart upon close inspection. This divide plays no small part in how difficult it is to properly learn mathematics outside of a mathematics department. Formalizing undergraduate math is important because it provides a solid foundation that leads to deeper understanding of mathematics when taken in aggregate across all participants. Even pure mathematicians have gaps once they step outside their field of expertise.
Well commented proofs are good to communicate intent but if you also want to be able to reproduce a similar proof, it's often useful to understand why tactics were deployed as they were. The existence of the wonderful https://plv.csail.mit.edu/blog/alectryon.html bears out the importance and utility of this.
> For understanding math
My contention, which I believe is shared by the article, is that this understanding is often flimsier than most think, particularly as one leaves well trafficked areas held together by tacit knowledge and knowledge of multiple reinforcing paths shared within communities with relevant expertise. However, even that is insufficient for less used lemmas.
This structuring of knowledge will be useful for mathematics education and research both, especially from the perspective of an individual human trying to safely use results of proofs.
> we really need tools to help us visualize structure of proofs
The output proof is a program, so the problem of visualizing proofs is much the same as visualizing programs and visual programming, sharing the same hurdles. Perhaps friendlier naming and formatting of output code in proof tools will be useful. I believe something more useful would be queryable visualizations of how theorems and lemmas connect and relate to each other.