[isaacfrond]

A few years back I made a concerted effort to learn Isabelle, the HOL based theorem prover. Proofs read a bit like natural languages but are fully rigorous, moreover Isabelle has application in math as well as programming. What's not to like.

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.

[robinzfc]

It was a similar experience for me when I tried to learn proving with Isabelle/HOL without an expert help. I gave up and switched to Isabelle/ZF and that was easy, my standard mathematics background was sufficient. I use a subset of the Isar language that is needed for my formalized mathematics hobby (shameless plug: isarmathlib.org). Of course if your goal is software verification, then Isabelle/HOL is the way to go. Btw, Isabelle is not "the HOL based theorem prover", Isabelle/HOL is just its most popular logic.

[6534278]

This is a bit out of my area but...

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

[practal]

I hear you. I picked up Isabelle relatively easily, but I had the good fortune to be at one of the places where Isabelle is developed, and actually became later part of that group for my PhD.

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.

[jksk61]

well, for lean I know there's a discord (with a fair amount of experts) and a fair share of resources nowadays. However, I did try 3 years ago and the jump between solving a simple algebra proof and contributing to Mathlib (or even understand something in it), is quite high.

Coq is well designed/easy to understand but it is missing a core mathlib like Lean. Moreover, most proofs are designed to "compile" quickly and not to be human readable.