Lean, Coq and other proof assistants: Visualising proofs as trees

What I found out was, that after diligently doing all the tutorials, and making all the exercises, there is still a huge gap between my skills and what is needed for real work. Note even that, you cannot even follow proofs of real theorems. Even with the reference manual in hand, trying to follow along word by word, there is a lot outright missing. From what I could gather, those that had successfully learned it did so at the hand of a master who explains the arcane incantations needed to get from proof state to proof state.

I'd still love to learn a formal theorem proving language, any one really, and be able to do formal proofs, but i'm not sure how. Coq seems even more arcane than Hol/Isabelle. I'm not sure about Lean, but I'm skeptical about learning it without having an expert on call.

Still, even for me, dealing with various issues in Isabelle is frustrating (I will not even touch stuff like Coq or Lean, these are just insults on my mathematical senses). I know how this all can be made more accessible and natural and practical, and I am working on it. I, too, want to be using such a tool for real stuff. In particular, integrating LLMs with theorem provers is very promising, and I think the new logic I am developing is especially suited for it. You could argue, but well, a natural language interface is just the surface, and the complexity remains just under this surface. I would not argue against that in principle, but my new logic hopefully also takes care of a lot of unnecessary complexity and complications under the hood.

> still a huge gap between my skills and what is needed for real work

That's kind of inevitable, you've passed your driving test but that doesn't mean you're ready to compete in Formula One race.

> Note even that, you cannot even follow proofs of real theorems

This may not be relevant to your experience or it may, but decades ago I did a tool-guided transformation of a very simple specification into a very simple program. This was done as a study for teaching people. I carefully explained every step as best I could, but the interesting thing was as my memory of doing it faded, the explanations became mainly useless – why I did a particular transformational step became lost, and my prior written explanations just didn't help. It's not like commenting code!

Now, maybe with extra experience I could do better these days, but quite possibly not. There is a certain kind of 'zone' you go into which has no parallel with programming. It may be that theorem proving at that level may only be something you can do, and do with practice, but can't follow afterwards; a state of mind. I don't know. FYI anyway.