# Exotic natural language summaries of formal proofs

Mathematical proofs written in natural language can often be used as guides to create formal proofs in proof assistants, depending on the level of detail of the proof and how many results and concepts it uses that have not already been written in the proof assistant. When this is done, the original proof serves as a natural language summary of the formal proof.

Sometimes the formal proof doesn't quite match the original proof, for example due to errors or skipped steps in the original proof. In these cases, as far as I know it's usually possible to straightforwardly modify the original proof to account for this modification.

But is it possible to construct natural language summaries of formal proofs that look very different from traditional natural language mathematics proofs, but still are readable to someone unfamiliar with the language?

For example, can people learn to use proof assistants without much exposure to traditional mathematics writing and then summarize their own work in new ways?

• I think this isn't exactly what you have in mind, but much of the HoTT Book was written by taking formalized proofs and figuring out how to write them in an informal language. Commented Feb 8, 2022 at 18:58
• This is a bit of a dual thing, but many large-scale formalization projects begin with a kind of blueprint, which aims to precisely lay down steps which will come into formalizing the result. For instance here is a blueprint for the recent Liquid Tensor Experiment. Commented Feb 9, 2022 at 0:21
• Actually, according to this blog post, my description above is not correct - the blueprint actually came after the proof was formalized. Commented Feb 9, 2022 at 2:09
• I can confirm that the name "blueprint" is not exactly optimal in the case of LTE. We had a rough start of a blueprint at the beginning of the project, but then worked mostly from Scholze's lecture notes for a couple of months. After finishing the key milestone, the blueprint was updated to contain a LaTeX version of the formalized proof.
– jmc
Commented Feb 9, 2022 at 7:44