New Foundations is consistent – a difficult mathematical proof proved using Lean
leanprover-community.github.io
leanprover-community.github.io
There is a serious danger, which has nothing to do with bugs in Lean, which is a known problem for software verification and also applies in math: one must read the conclusions carefully to make sure that the right thing is actually proved.
I read Wilshaw's final conclusions carefully, and she did indeed prove what needed to be proved.
Wilshaw's formalization is not vulnerable to this objection, though libraries were used. What is proved is that a certain defined concept satisfies a certain suite of formulas of first order logic. If there is a predicate satisfying that suite of formulas, NF is consistent.
human interaction helps create confidence. But the software is extremely reliable: a philosophical challenge based on bugs in theorem proving software just is not going to hold water.
Every definition and theorem in mathlib and this project have been checked by Lean’s trusted kernel, which computationally verifies that the proofs we have constructed are indeed correct. However, Lean cannot check that the statements of the definitions and theorems match their intended English equivalents, so when drawing conclusions from the code in this project, translation to and from English must be done with care.
LLMs can write better English, but the curating step is still critical, because it also produces a lot of garbage.
Remember, we're not talking about a static target here, and the post I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents. That's a long timeline on a rapidly moving target that is, as I said, already seems to be better than most humans at understanding and writing English.
Depends on the complexity, but for the simpler things I think I could get confident in a day or so. For more complex things, it might take longer to assess their ability.
But I'm not going to trust LLM blindly for anything.
> I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents.
I don't defend this strong claim and limit my answer to LLMs (and mostly just state of the art). OTOH I believe that trust will continue to be a big topic for any future AI tech.
Again, what does "blindly" mean? Suppose you went a month without finding a single issue. Or two months. Or a year. The probability of failure must literally be zero before you rely on it without checking? Are you applying the same low probability failure on the human equivalent? Does a zero probability of failure for a human really seem plausible?
Choosing to handle it yourself does not reduce probability of error to zero, but it does move the locus of consequence when errors occur. "you have nobody to blame but yourself".
One reason people might trust humans over AI regardless of failure rate is answering the questions "what recourse do I have when there is an error" compounded by "is the error model self-correcting": EG when an error occurs, does some of the negative consequence serve to correct the cause of the error or doesn't it.
With another human in the loop, their participation in the project or their personal honor or some property can be jeopardized by any error they are responsible for. On the one hand this shields the delegator from some of the consequence because if the project hemorrhages with errors they can naturally demote or replace the assistant with another who might not have as many errors. But on the other hand, the human is incentivized to learn from their mistakes and avoid future errors so the system includes some self-correction.
Using a static inference LLM, the user has little recourse when there is an error. Nowhere to shift the blame, probably can't sue OpenAI over losses or anything like that. Hard to replace an LLM doing a bad job aside from perhaps looking at ways to re-fine-tune it, or choose a different model which there aren't a lot of materially competing examples.
But the biggest challenge is that "zero self-correction" avenue. A static-inference LLM isn't going to "learn from its mistakes", and the same input + random seed will always produce the same output. The same input with a randomized seed will always produce the same statistical likelihood of any given erroneous output.
You'd have to keep the LLM on a constant RLHF fine tuning treadmill in order for it to actually learn from errors it might make, and then that re-opens the can of worms of catastrophic forgetting and the like.
But most importantly, that's not the product that is presently being packaged one way or the other and no company can offer any "learning" option to a single client at an affordable price that doesn't also commoditize all data used for that learning.
If the LLM required a constant fine-tuning treadmill, you wouldn't actually use it in this application. You could tell if you were on such a treadmill because its error rate wouldn't be improving fast enough in the initial phases while you were still checking its work.
As for what recourse you have in case of error, that's what fine-tuning is for. Your recourse is you change the fine-tuning to better handle the errors, just like you would correct a human employee.
Employees are not financially liable for mistakes they make either, just their job is at stake, but this is all beside the point, at the end of the day the only rational question is: if the LLM's error rate is equal to or lower than a human employee, why prefer the human?
till they incorporate more of what some of your writing and loose their advantages
Imagine someone saying "just write good English lol eventually you can do good math". I'm aware you're not quite saying this but you seem really distracted by the human language representation of math, connecting doing math proofs to generating English sentences from some probability distribution is ridiculous. Of course it is possible LLMs can do math, if it's matter of having nonzero chance, there's also a nonzero chance we are all brains in vats. More rationally if someone says something is possible they should produce some evidence that it is possible. And then we decide whether that evidence is good enough.
Writing well in any human language is not good enough, since it is entirely different from being able to tell whether a set of formal axioms capture certain ideas about a mathematical structure. This is a model theoretic issue. Neural network theorem provers deal with proof theoretic issue.
The best LLM-Lean provers right now are tackling the very challenging problem of how to generate the right sequence of tactics for infinite search space, all relying on, excuse me, undergrad students to formalize proofs and statements for them.
From a foundational perspective, it is also important to note that this proof is one of equiconsistency between NF and the Lean kernel, which itself is handchecked. Mechanized theorem provers preserve that level of correctness imputed to them via outside injection, from humans or other out-of-band systems.
They do exactly what you tell them to.
[1]: https://inutile.club/estatis/falso/
[2]: https://www.youtube.com/watch?v=sv97pXplxf0
[3]: https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
The trusted codebase becomes that checking algorithm, along with the "compiler" that translates the high-level language to term rewriting syntax. Formally verifying that codebase is a rather circular proposition (so to speak), but you could probably bootstrap your way to it from equations on a chalkboard.
Claimed to be proven in 2012, and to 400+ page paper is online. But I don't many accept the proof.
But Mochizuki's "proof" is completely impenetrable even to experts on, like, page 3, and makes no effort to explain what is happening.
Another key difference is that New Foundations is a niche field, so there simply was not a huge amount of human effort spent reading Holmes's work. That's not the case with Mochizuki's proof. There's a big difference between "a small number of mathematicians didn't understand the proof but suspect it's correct" and "a large number of mathematicians didn't understand the proof and concluded it was incorrect."
And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. Mochizuki's proof is not type-theoretic and does not seem like a great candidate for the calculus of constructions - maybe it is! I actually have no idea. I suspect Mochizuki is the only person in the world who can answer that. But it's critical that Holmes did so much background work to simplify his proof and make this Lean program possible. Mochizuki should do the same.
AFAICT, both in terms of the "sociology of mathematics" and the amount of work required to even attempt a Lean formalization, trying to verify Mochizuki's proof is a waste of time.
Further edit: I guess he's at Arizona right now, but he was at IAS at some point....
I am not so sure about this, actually. "twisted type theory" looks like type theory more in the original Bertrand Russel sense than in the modern (Martin Loef, Jean-Yves Girard, etc.) sense.
https://www.reddit.com/r/math/comments/1bhiz0s/construction_...
It would be nice if this one were formalized in Lean (or Coq or HOL) though.
But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
https://leandojo.org/ https://github.com/lean-dojo/LeanCopilot https://arxiv.org/abs/2404.07382
As far as making LLMs understand mochi math... I'm going to go out on a limb and say it will probably take less time for us to build an AI that understands mochi than it would take to understand mochi ourselves.
The progress isn't insane or miraculous. But it's moving the needle in an otherwise somewhat stagnant area. And that means we need to pay attention and update our beliefs and working theories.
IRT, the topic and digression here, LLM and LEAN4 are of not much use for IUT.
IUT Theory is much easier understood by a hacker than by a math guy, eventually tho, monitors and tv's did kinda become the same thing but there are, some minor differences.
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
I think the main thing is the existence of the universal set. For my use case, the type system of a programming language, such a universal set is very useful. There are various hacks used in existing systems like cumulative universes or type-in-type which are not as satisfying - instead, I can just check that the type signature is stratified and then forget about types having numerical levels.
the universe is a boolean algebra in NF: sets have complements, there is a universe.
The number three is the set of all sets with three elements (this is not a circular definition; it is Frege's definition from way back); in general, a cardinal number is an equivalence class under equinumerousness, defined in the usual set theoretic way, and an ordinal number is an equivalence class of well-orderings under similarity.
When you look at objects which lead to paradox (the cardinality of the universe, the order type of the natural well-ordering on the ordinals) then you discover the violence inherent in the system. Very strange things happen, which are counterintuitive. None of this depends on my proof to work: these are all features of NFU (New Foundations with urelements) which has been known to be consistent since 1969, and one can explore what is happening by looking at its known models, which are far simpler than what I construct.
Also, now I have to go learn about urelements too :-(
There is nothing mysterious about urelements: an urelement is simply an object which is not a set. To allow urelements is to weaken extensionality to say, objects with the same elements which are sets are equal; objects which are not sets have no elements (but may be distinct from each other and the empty set).
Allowing urelements can be viewed as a return to common sense :-)
I can't make up my mind if this is extremely elegant, or mindbogglingly horrendous; awesome or awful. I lean towards elegant, because the mindboggle caused by traditional set theory.
Another way to be introduced to New Foundations, along with how one can use it, is the Metamath database for New Foundations: https://us.metamath.org/nfeuni/mmnf.html
Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things.
One thing you immediately discover when you try to use New Foundations is that "the usual definition of the ordered pair, first proposed by Kuratowski in 1921 and used in the regular Metamath Proof Explorer, has a serious drawback for NF and related theories that use stratification. The Kuratowski ordered pair is defined as << x , y >> = { { x } , { x , y } }. This leads to the ordered pair having a type two greater than its arguments. For example, z in << << x , y >> , z >> would have a different type than x and y, which makes multi-argument functions extremely awkward to work with. Operations such as "1st" and complex "+" would not form sets in NF with the Kuratowski ordered pairs. In contrast, the Quine definition of ordered pairs, defined in definition df-op, is type level. That is, <. x , y >. has the same type as x and y, which means that the same holds of <. <. x , y >. , z >. This means that "1st" is a set with the Quine definition, as is complex "+". The Kuratowski ordered pair is defined (as df-opk), because it is a simple definition that can be used by the set construction axioms that follow it, but for typical uses the Quine definition of ordered pairs df-op is used instead."
One eye-popping result is that the Axiom of Choice can be disproven in NF. See that site (or other pages about NF) for details.
How is that not a problem? The type of a set needs to be higher than its elements to prevent the construction of a set containing itself. If a tuple is the same type as an elements, then can't you construct a tuple that contains itself as its first element, i.e. "x.0 = x" is a stratified formula so x exists.
I've only used lean a little bit but I'm pretty sure you can start lean with a blank slate, declare whatever you want and then build up from there. In fact the Natural Number Game[1] is basically this, you develop the Peano axioms etc and prove everything about the natural numbers from scratch without using the standard library (which obviously would have all that built in).
Metamath is much more configurable in this regard, you just directly specify the axiom system you want to work in and there is no special status given to first order logic or anything like that.
Like having a programming language sold as free of any awful metaprogramming constructions (and induced headaches) through guarantees that no metaprogramming at all can be done in it.
A language that forbids to talk about its own grammatical structures is doomed to see its users abandon or extend it when they will inevitably deal with a situation where exchanging about the communication tool at hand is required to appropriately deal with its possibilities, expectable behaviors and limits.
> A language that forbids to talk about its own grammatical structures
That's just not the case, and it's not what is being claimed here.
Which, to my mind, implies that an expression should not be allowed to embed an expression. Which is roughly equivalent to disallow a code to embed code written in the same language, let alone a code aware of the language structure and able manipulate the current code base abstract syntax tree or any equivalent facility.
Once again, I don’t claim this about NF, which I wasn’t aware of before this thread. I never dug into Quine’s work to be transparent on the matter.
ZF, by contrast, has eight rather ad hoc axioms/axiom schemes.
I barely understand anything from that discussion and don't practice any of them. Feel free to chime in if you have something about this, or a comparison with other proof assistants.
[1] https://proofassistants.stackexchange.com/questions/153/what...
I think proponents of Lean are a little bit too strong in their use of language. Lean is not a superior method of proof, as is often implied. It is an alternative way of proof. If one looks into getting into Lean, one quickly realizes this situation. It is a programming language and system, with its own bugs, and you are highly reliant upon various stacks of libraries that other humans have written. These libraries have choices made in them and potentially gaps or even bugs.
So I think I take issue with the language here that it was Lean that said the proof was good. I think the more accurate and honest language is that the written proof was verified by human mathematicians and that the proof was translated into Lean by humans and verified there as well. I don't think it's necessarily accurate, or I haven't seen explanations that say otherwise, that it's Lean that provides the sole, golden verification, but that is often implied. I think the subtitle is the most accurate language here: "A digitisation of Randall Holmes' proof".
> 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.
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.
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).
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).
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.
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
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.
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.
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.
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.
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.
It's true for all practical purposes. Humans are just running on protein, lipids and sugars, and these are far less reliable than transistors.
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.
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.
https://math.stackexchange.com/questions/1901133/euclids-ele...
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
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.
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.
As an amateur mathematician whose use of sets is mostly as a lingua franca for describing other things, it's not clear to me what implications this has for the wider mathematical field, especially if the usefulness of NF is comparable to the established ZFC and its variants. Is it expected to become as popular as ZFC in machine proofs?
I do find the existence of a universal set more intuitive, so if nothing else this proof has rekindled my own interest in formalisation.
1. We prove NF is inconsistent. Then ZFC is also inconsistent (and the stars start winking out in the night sky ;)
2. We prove ZFC is inconsistent. Then there's still a chance NF is consistent (fingers crossed!)
I'm probably ignoring more practical "quality of life" benefits of NF, like being able to talk about proper classes, and side stepping Russell's paradox with stratified formulas.
I wonder whether this will eventually lead to collaborative proofs , and ‘ bug fixes’ , essentially turning maths into a process similar to code on GitHub.
A few unwise life style choices later and I find myself running a small IT company for the last 25 odd years.
I'll never get beyond undergrad engineering maths n stats but it's works like GEB and the Natural Numbers Game (and I see there are more) that allow civilians like me to get a glimpse into the real thing. There is no way on earth I could possibly get to grips with the really serious stuff but then the foundations are the really serious stuff - the rest simply follows on (lol)
Whom or whoever wrote the NNG tutorials are a very good communicator. The concepts are stripped to the bare essentials and the prose is crystal clear and the tone is suitably friendly.
Top stuff.
(My making an easy fun game of proofs, I hope we can introduce them far earlier in the school curriculum. How many people in this world really understand the difference between reasoning and charismatic rhetoric? I don't blame anyone that isn't given the way we are taught.)
That said, if you have a system X, it can't prove it's own consistency, but a stronger system Y can prove its consistency (and perhaps some other stronger system can prove Y's consistency. This gives us a chain of systems, each proving the consistency of some weaker system).
That doesn't absolutely prove that the system is consistent--if Y was inconsistent, it could prove X is consistent (and also could prove that X is inconsistent). Nonetheless, it is still valuable. After all, part of our use of Y is the fact that we know of no inconsistency in it. And since formal systems often are subtly inconsistent, "consistent assuming some other system is consistent" is a lot better than "we have no proof whatsoever of consistency".
EDIT: I'm working under the hypothetical situation in which PA could prove its consistency. I know it can't but assuming that it could prove it's own consistency you still couldn't conclude that it was consistent since an inconsistent system can prove it's consistency.
The point being, having PA prove its own consistency couldn’t tell you anything of value even in the case that Godel’s theorems were not true. This is an interesting phenomenon. The only way to know a system is consistent is to know all of its theorems.
https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...
What distinction are you drawing? I see no contradiction between something being reality and something being an obstruction to be worked around.