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