I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards.

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.

No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious).

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

The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want.

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 originally intended to write what follows as its own comment but, although I used Coq instead of Lean and worked through a different set of exercises, your criticisms so closely mirrored mine, I decided to reply here instead, and point out promising paths to solutions.

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.

Actually there isn't much to understanding the tactics unless you want to use them similarly, just like you wouldn't bother looking into what "auto" has done. For understanding math it is a lot more important to understand the lemmas and why they are structured certain way, akin to understanding the API of programs. We can think of theorems as math's public API and lemmas the internal API for devs. In machine checked proofs lemmas often take on distinct flavors because how a human normally proves things may be hard to mechanize. Intead of tools for understanding tactics (granted, these could be useful for tacticians :) we really need tools to help us visualize structure of proofs. If I know how to write a lemma, tactical proof is rarely a blocking issue. Once it is checked the tactics become irrelevant. They were just there to convince the proof checker.

All what you say makes sense, especially as one becomes more comfortable with tactics but I maintain formal proofs are a lot harder to parse than regular math proofs. Having to write for both machine and human distorts a proof's natural flow and reading them often feels like trying to understand partially commented code by executing it in your head.

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.

The flimsiness of one's understanding tends to manifest as false "lemmas", which can't really be proved because one forgot certain conditions that are typically implicit with human understanding but must be made explicit formally. However if a proof can be completed then it's solid by definition. I would contend when a proof becomes hard to understand instead of documenting tactics one should break up the proof into more lemmas or create more subgoals; preferrably all tactics are "auto". It's nice that the tool you referred to is general and can be used to document any prospect of proof but being based on a markup language it is mostly static. When Gonthier mechanized Feit-Thompson Odd Order Theorem, he had very large graphs showing the relationship of the lemmas. Unfortunately those were also static as I remember and only really comprehensible to the experts. It would be nice to have interactive versions that can aid an average reader on comprehending and exploring the overall relationships. Such a tool is also sorely missing for understanding large code bases. The two are really two sides of the same coin through Curry-Howard. The good thing is a tool that lets users efficiently navigate structures can be done without extra effort of the proof writer (of course documenting intention is always important).