Formalising Mathematics: An Introduction

There is only one kind of proof by contradiction. Assume not P, derive a contradiction which implies not not P, then conclude (via excluded middle) P.

If you assume P, derive a contradiction, then conclude not P, that is a direct proof of negation not a proof by contradiction.

> However, AI works best with a database — and those databases are not yet there.

They do, but I would tell you that if that is your main motivation to create those databases, don't do it. The AI might spend milliseconds on work that takes man-years to compile, but get stuck on absolutely tiny issues of details it can't grok and which you can quickly explain.

If AI is the goal, I would propose to discuss with AI-researchers in the area of automated maths about what they can actually use to make progress. There are ways to have the AI learn unsupervised as much as possible, and to have it ask for supervision where needed.

In a similar way, it took a while to teach alphaGo to play go, but it only took a couple of extra years to have alphaZero play both go and chess without any database of example games.

I fully agree with the rest of the argument and I love the work that is being done to double check mathematics. But as AI researcher, I think this is a poor motivation and would warn against using it, as it might be very disappointing in the long run about how little of it turned out to be useful for AI.

I originally intended to write what follows as its own comment but, although I used Coq instead of Lean and worked through a different set of exercises, your criticisms so closely mirrored mine, I decided to reply here instead, and point out promising paths to solutions.

I too felt it a waste of time to prove things that were clearly "obvious". Of course, in math, some of the most frightening words to encounter are "obvious" and "trivial" but in this case it really was trivial, at the level of proving `a + b = b + a` while working with integers. Tactics like auto, tauto, ring and field help here and should be given more and earlier emphasis in teaching materials. Tactics like `auto` perform like the proof search you mention and others like ring and field make cleverer use of structure.

To fill in the rest of the gap, a project like the Lean math library goes a long way. Not having to provide your own implementation of reals, differential forms or vectors over reals or complex numbers is incredibly useful. I was surprised by how difficult it was to find (I never did) a well maintained and documented library of basic common mathematical structures in Coq.

The second major issue is Formal proofs without their contexts (something like a debugger variables watch list in regular type code), are incomprehensible to most. However, a project, https://plv.csail.mit.edu/blog/alectryon.html, for Literate Formal proofs fully addressed that pain point for me. It's curious how the problem of tedium has a clear path to solution in the Lean community and the equally important flaw of write only proofs is being addressed within the Coq community.

Returning to the issue of what is obvious, a vast amount of mathematical knowledge is tacit, buried in the minds of the respective communities of pure mathematicians. For everyone else, especially users who cannot themselves provide proofs, mathematical knowledge is very often like a Potemkin village. Superficial and artifice, understanding that falls apart upon close inspection. This divide plays no small part in how difficult it is to properly learn mathematics outside of a mathematics department. Formalizing undergraduate math is important because it provides a solid foundation that leads to deeper understanding of mathematics when taken in aggregate across all participants. Even pure mathematicians have gaps once they step outside their field of expertise.

If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more.

However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were checked. They were not confident of the result. And nobody has been able to review the proof.

This began a decades long effort, which is currently incomplete, to produce a second proof that is more understandable. That effort seems to have fizzled out.

So one of the most important results in mathematics in the 20th century does not have a proof that anyone can understand or review. And this is true despite a number of very smart people devoting their entire lives to the subject.

I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.