Desire for Lean proofs

Stream: general

[Martin Dvořák]

As my Ph.D. comes to a close, I attempted to reflect on what makes me want formal proofs and what I think makes other people want them. I identified two kinds of people who want proofs written in Lean (or formal proofs in general). Do you agree? Is there something important I missed? Would you add a third category?

1. Believers in the central dogma: Mathematicians generally hold the opinion that a mathematical proof is valid if and only if it could be rewritten into a formal proof (at least in principle — most mathematicians have absolutely no interest in actually doing it). In this light, a mathematical proof becomes trustworthy in one of the following two ways; either a human expert carefully reads the proof and affirms that she believes that the proof is valid (in the sense that she believes that a formal proof could be written in principle by following the mathematical proof), or a formal proof is written and verified by a computer (which is generally considered to be the hard way to convince the sceptics). Therefore, given that the notion of formal proofs has been defined (and the computer programs that check them have been implemented) so that they formalize what is considered to be the validity of mathematical proofs, the Lean proof is useful because the Lean proof convinces the mathematical community that the mathematical proof is valid, which is what they are ultimately interested in (i.e., the mathematical proof is what satisfies them; the formal proof is just a replacement for a human reviewer of the mathematical proof (or, more accurately, formalization is the vehicle that allows human reviewers to be replaced by computer checkers)). For believers in the central dogma, a formal proof can be a substitute witness but not the objective.
2. Formalists: I get satisfaction from Lean proofs. Mathematical proofs don't do it for me. I view mathematical proofs as something that is useful precisely because they provide guidance on how to write a formal proof. However, it is the proof written in Lean that ultimately satisfies me. For me, personally, writing a mathematical proof without formalizing it feels like putting a piece of delicious food into my mouth but spitting it out instead of chewing and swallowing it — it teases me but doesn't provide any satisfaction in the end.

[Julian Berman]

There is Patrick Massot's *Why Formalize Mathematics* on this subject.

[Martin Dvořák]

How embarrassing that I missed it! I thought I had read all the important essays on this topic. Obviously not!

[suhr]

• I believe fine details deserve to be preserved, and formal proofs allow to preserve them
• I believe that having a real notion of a proof being complete is valuable
• I believe that having a library of mathematics where every result can be inspected as deeply as you need to is valuable
• I like interactivity

I wonder which category this should go to.

[Snir Broshi]

Martin Dvořák said:

I identified two kinds of people who want proofs written in Lean (or formal proofs in general). Do you agree? Is there something important I missed? Would you add a third category?

If your goal is to describe all kinds, I'll mention that I don't see myself in either category, but leaning towards the first one. Here's how I'd describe why I want formal proofs:

• I like the promise of correctness
• I like the idea of software watching my back
• I really really like the goal of cataloguing most maths (a la ProofWiki) and getting rid of the messy unindexed pile of PDFs
• I wish for the future where ITPs are maths, where writing a paper proof doesn't count as properly doing math research
• I also see Mathlib as the next logical step from a computer-algebra-system (e.g. Sympy, Mathematica, GAP), even though it isn't close to subsuming them

[Snir Broshi]

I also remember there being a series of blog posts somewhere, one of which was about this?

[Martin Dvořák]

suhr said:

I wonder which category this should go to.

I might have given a slightly false impression that my post elaborates on why I want to work on Lean proofs. However, I elaborated on why I want to have Lean proofs — it could be also framed as why I want to download a Lean repository rather than downloading a PDF from arXiv.

I talk a lot about why I want to work on Lean proofs in my thesis, but the post above is about why I want to have Lean proofs.

[Snir Broshi]

Oh there was also this message recently #Lean for teaching > Teaching with Verbose Lean @ 💬 which I love, about ITPs being the future rather than an appendix for correctness

[Martin Dvořák]

OMG, the comments made me find two absolutely amazing pieces of writing! I'll save them to reread in the future.

[Violeta Hernández]

I've been learning about surreal numbers as I've been formalizing them, and I've discovered a lot of subtleties within its arguments which the literature seems to have largely ignored. And in that process I feel like I've gained a much deeper understanding on the subject.

[Timothy Chow]

In Patrick Massot's section on "Creating," he says that creating new theorems is mostly science fiction with current day technology. I agree, but I think that the day may not be too far off when the combination of ITPs with various types of artificial intelligence leads to computers creating genuinely new mathematics. There is a lot of discussion of this topic in the "Machine Learning for Theorem Proving" channel.

I also like to point to the Holmes-Wilshaw formal proof of the consistency of NF as an example where the Lean proof broke a sociological logjam. No referee could be found to invest the time required to validate Holmes's proof when there was still significant doubt about whether the argument was fundamentally correct. The ITP provided a clear goalpost that Holmes needed to meet and that would persuade others if met. This was a case where informal standards of mathematical rigor were not sufficient to lead to a resolution.

[A.]

Martin Dvořák said:

Is there something important I missed? Would you add a third category?

The whole verified software thing? I think that was a big motivation for the creators of Lean.

For certain types of software one might find oneself proving theorems qualitatively similar to those we see in Mathlib but too niche to be of general interest.

[suhr]

The proof of the consistency of NF is also an example of a proof where management of details is essential. Without a proof assistant it was hell to write and verify, but Lean made it quite manageable.

[Timothy Chow]

Martin Dvořák said:

How embarrassing that I missed it! I thought I had read all the important essays on this topic. Obviously not!

If you're not already aware of it, Donald Mackenzie's book Mechanizing Proof is well worth reading.

[GasStationManager]

The reason I (a non-mathematician) became interested in Lean is because of its potential for AI safety. As AIs become smarter, and able to produce sophisticated outputs (software code, and soon enough, research), I see ITPs like Lean as an essential tool that allows the possibility that humans can trust the outputs of (superintelligent) AIs, without having to understand and check every detail of the output. There's an essay I wrote a year ago; the technical details may have become slightly outdated, but the motivation remains.