4
$\begingroup$

There are extensive libraries of formalized mathematics like those of Lean, Coq or Isabelle/HOL. What I am interested in is documents of formalized mathematics that closely follow certain informal works, e.g. an undergraduate textbook. Ideally, the formalized document would contain all the mathematical content of the informal source text, including proof steps, and contain additional material required to make the document fully formal (e.g. additional proof steps and lemmas that were implicitly assumed in the source text). The connections between the informal statements and the corresponding formalizations should be made explicit.

I call this a "bilingual corpus" of formal and informal mathematics, because it reminds me of the idea of a bilingual corpus of translated texts, which can be used for training automated translation tools. But the potential benefit for training machine learning models is not the only reason why I am interested in such a "bilingual corpus" of formal and informal mathematics. I also believe that the creation and study of such documents can increase our understanding of how mathematicians actually do mathematics and what one needs to take care of if one wants to develop tools for formalizing mathematics that aim at being more natural for mathematicians.

Now my actual questions:

  1. Does anybody know of a piece of formalized mathematics that follows an informal source text as closely as described above?
  2. Can anybody recommend fragments of existing libraries of formalized mathematics that have a closer connection to specific source texts than the average documents that can be found in such libraries?
$\endgroup$
4
  • $\begingroup$ You can have a look at the blueprint of the Liquid Tensor Experiment and similar projects. $\endgroup$
    – Ricky
    Jan 26, 2023 at 20:30
  • $\begingroup$ The Xena project was motivated in part by the lack of such a "bilingual corpus." Kevin Buzzard lamented that formalized mathematics was a disorganized hodgepodge of isolated results. He wanted to create a library of "standard results" starting from the ground up (i.e., including the entire undergraduate curriculum). That dream remains unrealized, but you might find some of what you're looking for in the student projects. $\endgroup$ Jan 28, 2023 at 14:28
  • $\begingroup$ Part of the problem is that existing texts aren't very suitable for formalization "as is." In the process of formalizing them, one typically finds that the informal treatment is very uneven from a formal point of view; things that seem too obvious to dwell on in an informal account may require considerable formal work. Also, what do you do when your informal text cites some other informal text that hasn't yet been formalized? In short, while I think your vision is a good one, there are some serious practical obstacles. That's why what you're looking for doesn't really exist currently. $\endgroup$ Jan 28, 2023 at 14:28
  • $\begingroup$ There is an interesting sounding book by Ganesalingam about the precise meaning of informal math. I haven't read it yet though: maa.org/press/maa-reviews/the-language-of-mathematics $\endgroup$
    – none
    Jan 29, 2023 at 3:45

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.