Hacker News Reader

I do think that machine-verified proofs in strong systems like Lean are far superior to proofs merely verified by humans. Humans are amazing, but they also get bored and miss details.

This isn't just a theoretical claim. People read Euclid's Elements for over two thousand years before noticing a missing axiom. That's the sort of basic mistake that any properly-working machine proof verification system would immediately reveal. Published math proofs are often later revealed to be wrong. The increasing sophistication of math means it's getting harder and harder for humans to properly verify every step. Machines are still not as good at creating proofs, but they're unequalled at checking them.

There are "competing" systems to Lean, so I wouldn't say that Lean is the "one true way". I like Metamath, for example. But the "competition" between these systems needs to be in quotes, because each has different trade-offs, and many people like or use or commit to multiples of them. All of them can verify theorems to a rigor that is impractical for humans.

For the curious: I assume the parent is referring to Pasch's axiom.

https://math.stackexchange.com/questions/1901133/euclids-ele...

Correct. The good news that Elements still works otherwise, you just need to add the missing axiom.

But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't.

Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people:

* metamath.exe aka Cmetamath (the original C verifier by Norman Megill)

* checkmm (a C++ verifier by Eric Schmidt)

* smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear)

* mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro)

* mmverify.py (a Python verifier by Raph Levien)

For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md

While there indeed may be bugs, it's my understanding that any trust needs to be placed only on the kernel.

> various stacks of libraries that other humans have written

If you're referring to mathlib here, I'm not sure this is correct. As again all mathlib code compiles down to code that is processed by the kernel.

Indeed this is reinforced by the draft paper on the website [0]:

> Lean is a large project, but one need only trust its kernel to ensure that accepted proofs are correct. If a tactic were to output an incorrect proof term, then the kernel would have the opportunity to find this mistake before the proof were to be accepted.

[0]: https://zeramorphic.github.io/con-nf-paper/main.l.pdf

I think their point is it’s turtles all the way down. At some point you’re relying on software, kernel or otherwise, which will always have the possibility for bugs.

It seems like Lean is an interesting tool that maybe could help with proving, but ultimately will never be authoritative itself as a statement of proof.

Of course, this is ultimately a philosophical debate, which hinges on the fact to at while Lean may be demonstrably correct in any number of known applications, there are no guarantees that it is and will remain correct. Such is the nature of software.

Such is the nature of math as well.

I’m not a mathematician, so I’d be interested in any perspectives if the two are ultimately so similar in this regard, or is there is something foundationally different about the traditional mathematical approach.

I suppose any proof is ultimately a matter of review and consensus, and potentially would rely on some fundamentally unprovable assumptions at a basic level (e.g. the underlying laws of the universe).

It is a fundamentally different manner. Proofs in Lean are formal all the way down. The kernel checks the validity of a proof. This is a finite program checking the validity of the kernel to high degree once is different to checking the validity of every new paper that comes out to high degree.

Yes, the human effort of checking proofs written in Lean is O(1) as you only need to verify the kernel. The human effort of checking proofs written traditionally is O(N). Of course writing proofs in Lean is much more difficult (for now) and, checking the proof is not the only interesting part. Other mathematicians also want to understand the proof, and this will always be O(n).

Also, while it's true that bugs in mathlib cannot cause lean to accept invalid proofs as long as the kernel is correct, bugs in mathlib can still be annoying (I have only used lean briefly and I got stuck for a long time on a buggy tactic that was silently messing up my proof state).

My personal belief is that translating an informal proof from a paper to a proof in Lean, given that the prerequisites are already formalized, is an O(n) operation where n is the length of the proof. It's just translation. Right now the constant is something like 10-100, but I think with more work on matlib and AI assistance it can be brought down to maybe 1-3, meaning formalising proofs right as you write them becomes feasible. In fact the constant may go below 1 as formalization in Lean can prevent unseen errors from slowing your progress.

What I was referring to is that we don't know if ZFC, for example, is consistent. And it is only consistent if there are unprovable statements. And of course, you can't know which statements are unprovable (because then you would prove its consistency). So, in some sense you're always chasing your own tail. Theorems might be proven true only because ZFC is inconsistent and therefore everything can be proven.

The Lean language is known to be equivalent to ZFC + {existence of n < omega inaccessible cardinals}, which is roughly the common language of mathematics. The actual implementation of the kernel _may_ have bugs, but that's sort of separate from the language definition.

The sentiment I see for the purpose of Lean now and in the near future is for more collaborative mathematics. Theorems and structures are more transparent and concrete (the code is right there). Results are more consumable. The community does not seem to see its main purpose being a way to quell doubts of a paper proof.

I think the counterpoint is it's turtles all the way down. At some point you're relying on human mind, logic or otherwise, which will always have possibility of misunderstandings and mistakes.

It seems like Mahematicians are interesring tools that maybe could help with proving, but ultimately will never be authorative itsel as a statement of proof.

Of course, this is ultimately a philosophical devate, which hinges on the fact to at while Mathematicians may be demonstrably correct in any number of known applications, there are no guarantees that they are and will remain correct. Such is the nature of wetware.

---

development of proof assistants is in noticable part fueled by the same fear - fear that wetware had a fault somewhere in the long ladder of math, causing all the layers above be a useless junk

and those things did happen, it isn't just an imagined threat

what proof assistants propose is a clever trick - write one, simple, kernel. Stare at those 100 lines of code. Stare at mathematical definitions of intended API. Conclude that those coincide. Then use that kernel on the text files with all the proof ladder

All mistrust of "whole mathematics" gets condensed in mistrust of 100 lines of code

And mistrust of wetware gets replaced with mistrust of hardware - something we already do since even before computers appeared

I think that's an overly formalistic view by the Lean team.

When I looked into Lean last (sometime last year), it was a hodgepodge of libraries and constructions. The maturity of the library depended upon if someone in that area of math had spent a lot of time building one up. There were even competing libraries and approaches. To me, that implies that there's "choice" there, just as there is in mathematics. And a choice could be "buggy". What's to say that the construction of a mathematical structure in Lean is the same as the mathematical structure in "normal" mathematics?

So yes, if that statement by the Lean team is accurate, you can build correct things on top of the kernel, but the use of "correct" is a very formal one. It's formally correct in terms of the kernel, but it doesn't mean that it's necessarily mathematically correct. This is to my understanding of course, garnered from trying to get into Lean.

From my understanding, the libraries written in Lean are also formally proven by the kernel. They may be hodge-podge or incomplete, but they are (by construction) not "buggy" in a way that could lead to incorrect proofs, right?

But like, you can look at what parts of Mathlib this development imports, it's mainly stuff imported by files in this subdirectory https://github.com/leanprover-community/con-nf/tree/main/Con... , and it's pretty basic things: the definition of a permutation, a cardinal number etc. Almost all of these are things that would feature in the first one or two years of an undergraduate math degree (from just quickly scanning it, the most advanced thing I could see is the definition of cofinality of ordinals). It seems practically impossible to me that someone would make a mistake when e.g. defining what a group is, in a way subtle enough to later break this advanced theorem. If you think that people could mess up that, then all of math would be in doubt.

Your analogy to buggy implementations in ordinary programming languages is deeply flawed though.

The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven.

Bugs at the library level can only appear in the form that formally stated theorems might not be what you think they are.

So I object to your characterization that they might be mathematically incorrect. The mathematical content might be different than believed though.

> The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven.

That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper.

Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.

> Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on;

Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further.

> (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.

A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.

Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem.

If the runtime is correctly executing the program, then the theorem is proven from the axioms.

Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter.

So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime.

And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.

> That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper.

It's true for all practical purposes. Humans are just running on protein, lipids and sugars, and these are far less reliable than transistors.

I think you are misunderstanding the relationship between the theorem and the proof. You express doubt that the proof is a good one, but then you point to the libraries in Lean as a possible source of incorrectness. The libraries cannot be the source of incorrectness in the proof. They can only be the source of incorrectness in the statement of the theorem. That's why others are challenging you to declare that you don't trust the Lean kernel. A kernel bug is the only thing that can permit incorrectness in the proof.

The exact content of the proof doesn't matter for the purposes of deciding whether you should believe the theorem. At all. What matters are two things: 1) Is the theorem correctly stated? That is, does it say what it's supposed to say in the agreed upon (natural or programming) language? 2) Do you trust the Lean kernel (or human reviewer of the proof, if applicable)?

If you accept 1) and 2), then you must accept the truth of the theorem.

No library used in the construction of the proof, nor any library used in the expression or the proof, can make or break the result.

If one uses a library in the statement of the theorem, then that matters. That's letting someone else define some of the terms. And one must investigate whether those definitions are correct in order to decide whether the theorem is stated correctly. If you wish to challenge the work on these grounds, by all means proceed. But you can't say you don't think the proof is a good one for such reasons.

The difference is that in lean you only need to trust the kernel. The rest is constructed on top. If the kernel is sound everything else is as well. This is in stark contrast with a standard programming language. Where at any time a bug can be introduced. It's also in stark contrast with math where any lemma may contain an error.

> It is a programming language and system, with its own bugs

The cool thing about theorem provers is that an invalid proof won’t even compile (as long as the kernel is correct). There’s no such thing as a traditional software bug that happens only at runtime in these systems when it comes to proofs, because there’s no runtime at all.

You can also use Lean as a “regular” programming language, with the corresponding risk of runtime bugs, but that’s not happening here.

You misunderstand theorem provers. This isn't kid "all abstractions leak" land -- you do not need to trust the libraries, you only need to trust the kernel.

Trusting the kernel is not trivial either, but this is still a major leap over informal proofs. With informal proofs you do in fact need to trust the "libraries" (culture, the knowledge of other people), because there is no practical way to boil down to axioms.