[Cybiote]

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.

[fspeech]

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.

[Cybiote]

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.

[fspeech]

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