[robinzfc]

Another aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why they are true, but it is close to impossible for a reader to see what is going on in the proof without running the script step by step in software. The Mizar proof language and Isabelle/Isar were designed to communicate as well and proofs written in those languages can be read and understood directly by humans. For a comparison how the same proof of a simple theorem looks like in Lean, Isabelle/HOL, Isabelle/ZF and Mizar see [1], [2] and [3].

[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijecti...

[2] https://isarmathlib.org/func1.html#a_bij_def_alt

[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html

[practal]

That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right.

I think the future looks like this: The resulting text will be natural language (LLM powered), layering upon the actual formal logic. I think Abstraction Logic is actually best suited for this scenario, and I am designing Practal from scratch for it.