13
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented Feb 8, 2022 at 18:58
  • $\begingroup$ 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. $\endgroup$
    – Wojowu
    Commented Feb 9, 2022 at 0:21
  • $\begingroup$ Actually, according to this blog post, my description above is not correct - the blueprint actually came after the proof was formalized. $\endgroup$
    – Wojowu
    Commented Feb 9, 2022 at 2:09
  • 1
    $\begingroup$ 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. $\endgroup$
    – jmc
    Commented Feb 9, 2022 at 7:44

1 Answer 1

Reset to default
6
$\begingroup$

It is certainly possible to generate summaries of formal proofs that are readable by people familiar only with the standard mathematical vernacular. Some formal proof languages like Naproche, Isar or Mizar are designed to look like traditional natural language mathematics proofs. For these languages the problem is trivial - the proofs written in them can be their own summary, with possibility of further improvement by the presentation layer. For others like Coq or Lean verification scripts the problem is more difficult, but I am sure it is not intractable.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I know Coq had Czar, a Mizar-mode which sadly never caught on. $\endgroup$
    – Alex Nelson
    Commented Feb 9, 2022 at 20:27
  • $\begingroup$ I guess this technically doesn't count as a summary as a summary should be shorter than the original, but it's very interesting! I had heard of Mizar but didn't realize that's how it worked. $\endgroup$
    – Will Sawin
    Commented Feb 10, 2022 at 20:45
  • $\begingroup$ The length of the summary is addressed in "further improvement by the presentation layer". For a structured proof language the presentation layer can allow the reader to set the desired level of detail - from theorem assertions only, through the main points of the proof, to the full details. $\endgroup$
    – Slawomir K.
    Commented Feb 11, 2022 at 15:14

Not the answer you're looking for? Browse other questions tagged or ask your own question.