10 ms·

New Foundations is consistent – a difficult mathematical proof proved using Lean

340 points by namanyayg 3y ago

stogot 3y ago
Do the incompleteness theorems not apply here?
- lmm 3y ago
  They start with a large cardinal assumption which is the usual workaround - you have a proof that this theory is consistent if a large cardinal like that exists, which is something you can't prove within the theory.
  - randallholmes 3y ago
    It's not really a workaround. Whenever we are proving the consistency of a theory T, we are implicitly working in a stronger system. That is just how consistency proofs are done. The incompleteness theorems do not say that we cannot prove the consistency of theories, or build models of theories...in a generally accepted theory such as ZFC. They do say that if we want to prove the consistency of ZFC itself we would need to work in an even stronger system.
    - randallholmes 3y ago
      and we really don't use a large cardinal assumption...the existence of beth_omega_1 is really small potatoes. But, it is stronger than NF.
    - lmm 3y ago
      How is that not a workaround? It's "just how consistency proofs are done" because it's a standard, popular workaround for the problem. We absolutely would prove consistency of ZFC and similar theories in ZFC if we could, we only work in stronger systems because we have to.
      - randallholmes 3y ago
        You don't work around what is impossible. A consistency proof for a theory T is usually a construction of a model of that theory in some context we have confidence in. Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality. And there are strong systems we have confidence in.
        lmm 3y ago
        > Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality. What distinction are you drawing? I see no contradiction between something being reality and something being an obstruction to be worked around.
      - randallholmes 3y ago
        I have the same objection when people talk about defining set theories in such a way as to avoid the paradoxes. We don't avoid or work around the paradoxes: they are mistakes. We simply do things correctly, we do what we can do.
YoshiRulz 3y ago
ZFC is dead, long live NF..? 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.
- barfbagginus 3y ago
  From my naive and amateur view, the relative consistency result makes NF at least as useful as ZFC, since every model of ZFC can be extended into a model of NF. But it seems it won't make NF all that useful unless: 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.
- randallholmes 3y ago
  It is no part of my agenda to promote the use of NF as an independent foundational system. It is a very odd one. But if someone wants to promote this, the consistency result says, it will work, at least in the sense that you are in no more danger of arriving at a contradiction than you are in ZFC.
seanhunter 3y ago
This is a fantastic result, congratulations!
user070223 3y ago
See also discussion on reddit with one of the creators.[0] https://old.reddit.com/r/math/comments/1ca6bj8/new_foundations_consistency_proof_now_partially/ https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...
- randallholmes 3y ago
  we are both in that conversation :-)
_jcrossley 3y ago
I wish I had the free time to keep up with the mathlib project - this is so cool. Is there any way someone can get involved in a super hands-off way?
- isaacfrond 3y ago
  You could start with the Natural numbers game. https://adam.math.hhu.de/#/g/leanprover-community/NNG4 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
  - gerdesj 3y ago
    Well, thanks a lot! One minute I'm setting up a monitoring system and then ... I've just proved two is the number after the number after zero \o/ 8)
    - _jcrossley 3y ago
      Hope you keep going with it, it’s a blast!
      - gerdesj 3y ago
        I read "GEB" by Hofstadter after I finished my A levels (UK, aged 18). I picked up a random book in the school library to fill in 20 mins before going out on a pub crawl (as you do). Once we had finished off the Abingdon Ock Street crawl in fine style and the hangover had subsided, I devoured it. I'd never read anything like it before - what a communicator of ideas. 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.
cwzwarich 3y ago
If I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were some previous projects (e.g. the Four Color Theorem in Coq) that validated existing proofs with a large computational element handled by untrusted software, but I think this is the first one where the epistemological status of the result was uncertain in the larger mathematical community.
- isaacfrond 3y ago
  Next up the abc-conjecture! Claimed to be proven in 2012, and to 400+ page paper is online. But I don't many accept the proof.
  - nicklecompte 3y ago
    There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Holmes really tries to make the reader understand, with a fairly gentle/apologetic introduction. 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.
    - 3y ago
xylol 3y ago
I'm really not from the field but wasn't there some Gödel theorem showing every system strong enough cannot show its own consistency?
- peteradio 3y ago
  I don't think the system here is trying to prove any of its underlying assumptions, just building on some set of existing ones. I doubt the theorem you are thinking of is applicable.
- pulisse 3y ago
  The system isn't being used to prove its own consistency. The consistency is proved in a different, stronger system.
- hyperpape 3y ago
  Gödel's incompleteness theorems are what you're thinking of. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... 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".
- deleted 3y ago
  [deleted]
- skhunted 3y ago
  What’s interesting to note is that even if a strong system could prove its own consistency then it wouldn’t tell you anything. An inconsistent system can prove its own consistency. So if a system has a proof that it is itself consistent then you still wouldn’t know if it is consistent.
einpoklum 3y ago
Can someone give a rough description of what is special, or novel, in the "New Foundations" set theory formulation, relative to other formulations? Or at least, link to a description readable by, say, a math undergrad student or an engineering professional?
- thefringthing 3y ago
  One "nice" thing about NF is that it has only two axioms/axiom schemes: 1) sets with the same members are the same, and 2) any stratifiable property corresponds to a set off all the things which have that property. And the definition of "stratifiable" isn't very complicated. ZF, by contrast, has eight rather ad hoc axioms/axiom schemes.
- Mathnerd314 3y ago
  I was just editing the Wikipedia article, it should be more readable now: https://en.wikipedia.org/wiki/New_Foundations https://en.wikipedia.org/wiki/New_Foundations 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.
  - randallholmes 3y ago
    It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
    - randallholmes 3y ago
      to the original poster, 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.
bmitc 3y ago
> Randall Holmes has claimed to have a proof of its consistency. In this repository, we use the interactive theorem prover Lean to verify the difficult part of his proof, thus proving that New Foundations is indeed consistent. 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".
- Ericson2314 3y ago
  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.
- enricozb 3y ago
  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 https://zeramorphic.github.io/con-nf-paper/main.l.pdf
Agingcoder 3y ago
I very much like this. I wonder whether this will eventually lead to collaborative proofs , and ‘ bug fixes’ , essentially turning maths into a process similar to code on GitHub.
- trenchgun 3y ago
  Already is. Check Lean blueprints. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
- practal 3y ago
  Yes, this idea of collaborative proofs has been around for a while now, at least for 10 years: https://arxiv.org/abs/1404.6186 https://arxiv.org/abs/1404.6186
randallholmes 3y ago
I would say that there is very little danger of a proof in Lean being incorrect. 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.
- spindle 3y ago
  Many congratulations on being formally proved right, Randall!
- mckirk 3y ago
  That's always the problem with these pesky computers. They do exactly what you tell them to.
- sn41 3y ago
  Congratulations on the verification of your proof! It must be great to have your research life's crowning work being formally confirmed! Also a great victory for the new foundations of Quine.
  - randallholmes 3y ago
    I have shown the consistency of New Foundations. My aim is not actually to promote it as a working set theory. NFU, which admits Choice, is probably better for that. But if there are people who want to use NF as the foundation, it is now seen to be as secure as a rather small fragment of ZFC.
- Strilanc 3y ago
  Another danger is some sort of bug in Lean itself. This isn't unprecedented in theorem provers [1][2]. These might be hard to hit by accident... but there are larger and larger collaborations where arbitrarily people fill in steps (like [3]). Someone trolling one of these efforts by filling a step in using a bug they found might become worth worrying about. [1]: https://inutile.club/estatis/falso/ https://inutile.club/estatis/falso/ [2]: https://www.youtube.com/watch?v=sv97pXplxf0 https://www.youtube.com/watch?v=sv97pXplxf0 [3]: https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
jraph 3y ago
I was wondering what were the fundamental differences between Coq and Lean and if they operated on the same kind of logic and found this [1]. 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-are-the-main-differences-between-coq-and-lean https://proofassistants.stackexchange.com/questions/153/what...
- xvilka 3y ago
  There are, you can check this discussion [1] as well. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871

340 points by namanyayg 3y ago

stogot 3y ago

Do the incompleteness theorems not apply here?

lmm 3y ago
They start with a large cardinal assumption which is the usual workaround - you have a proof that this theory is consistent if a large cardinal like that exists, which is something you can't prove within the theory.
- randallholmes 3y ago
  It's not really a workaround. Whenever we are proving the consistency of a theory T, we are implicitly working in a stronger system. That is just how consistency proofs are done. The incompleteness theorems do not say that we cannot prove the consistency of theories, or build models of theories...in a generally accepted theory such as ZFC. They do say that if we want to prove the consistency of ZFC itself we would need to work in an even stronger system.
  - randallholmes 3y ago
    and we really don't use a large cardinal assumption...the existence of beth_omega_1 is really small potatoes. But, it is stronger than NF.
  - lmm 3y ago
    How is that not a workaround? It's "just how consistency proofs are done" because it's a standard, popular workaround for the problem. We absolutely would prove consistency of ZFC and similar theories in ZFC if we could, we only work in stronger systems because we have to.
    - randallholmes 3y ago
      You don't work around what is impossible. A consistency proof for a theory T is usually a construction of a model of that theory in some context we have confidence in. Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality. And there are strong systems we have confidence in.
      - lmm 3y ago
        > Godel's theorem shows that that context has to be stronger than T. This isn't some kind of obstruction, it is reality. What distinction are you drawing? I see no contradiction between something being reality and something being an obstruction to be worked around.
    - randallholmes 3y ago
      I have the same objection when people talk about defining set theories in such a way as to avoid the paradoxes. We don't avoid or work around the paradoxes: they are mistakes. We simply do things correctly, we do what we can do.

YoshiRulz 3y ago

ZFC is dead, long live NF..? 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.

barfbagginus 3y ago
From my naive and amateur view, the relative consistency result makes NF at least as useful as ZFC, since every model of ZFC can be extended into a model of NF. But it seems it won't make NF all that useful unless: 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.
randallholmes 3y ago
It is no part of my agenda to promote the use of NF as an independent foundational system. It is a very odd one. But if someone wants to promote this, the consistency result says, it will work, at least in the sense that you are in no more danger of arriving at a contradiction than you are in ZFC.

seanhunter 3y ago

This is a fantastic result, congratulations!

user070223 3y ago

See also discussion on reddit with one of the creators.[0] https://old.reddit.com/r/math/comments/1ca6bj8/new_foundations_consistency_proof_now_partially/ https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...

randallholmes 3y ago
we are both in that conversation :-)

_jcrossley 3y ago

I wish I had the free time to keep up with the mathlib project - this is so cool. Is there any way someone can get involved in a super hands-off way?

isaacfrond 3y ago
You could start with the Natural numbers game. https://adam.math.hhu.de/#/g/leanprover-community/NNG4 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
- gerdesj 3y ago
  Well, thanks a lot! One minute I'm setting up a monitoring system and then ... I've just proved two is the number after the number after zero \o/ 8)
  - _jcrossley 3y ago
    Hope you keep going with it, it’s a blast!
    - gerdesj 3y ago
      I read "GEB" by Hofstadter after I finished my A levels (UK, aged 18). I picked up a random book in the school library to fill in 20 mins before going out on a pub crawl (as you do). Once we had finished off the Abingdon Ock Street crawl in fine style and the hangover had subsided, I devoured it. I'd never read anything like it before - what a communicator of ideas. 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.

cwzwarich 3y ago

If I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were some previous projects (e.g. the Four Color Theorem in Coq) that validated existing proofs with a large computational element handled by untrusted software, but I think this is the first one where the epistemological status of the result was uncertain in the larger mathematical community.

isaacfrond 3y ago
Next up the abc-conjecture! Claimed to be proven in 2012, and to 400+ page paper is online. But I don't many accept the proof.
- nicklecompte 3y ago
  There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Holmes really tries to make the reader understand, with a fairly gentle/apologetic introduction. 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.
  - 3y ago

xylol 3y ago

I'm really not from the field but wasn't there some Gödel theorem showing every system strong enough cannot show its own consistency?

peteradio 3y ago
I don't think the system here is trying to prove any of its underlying assumptions, just building on some set of existing ones. I doubt the theorem you are thinking of is applicable.
pulisse 3y ago
The system isn't being used to prove its own consistency. The consistency is proved in a different, stronger system.
hyperpape 3y ago
Gödel's incompleteness theorems are what you're thinking of. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... 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".
deleted 3y ago
[deleted]
skhunted 3y ago
What’s interesting to note is that even if a strong system could prove its own consistency then it wouldn’t tell you anything. An inconsistent system can prove its own consistency. So if a system has a proof that it is itself consistent then you still wouldn’t know if it is consistent.

einpoklum 3y ago

Can someone give a rough description of what is special, or novel, in the "New Foundations" set theory formulation, relative to other formulations? Or at least, link to a description readable by, say, a math undergrad student or an engineering professional?

thefringthing 3y ago
One "nice" thing about NF is that it has only two axioms/axiom schemes: 1) sets with the same members are the same, and 2) any stratifiable property corresponds to a set off all the things which have that property. And the definition of "stratifiable" isn't very complicated. ZF, by contrast, has eight rather ad hoc axioms/axiom schemes.
Mathnerd314 3y ago
I was just editing the Wikipedia article, it should be more readable now: https://en.wikipedia.org/wiki/New_Foundations https://en.wikipedia.org/wiki/New_Foundations 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.
- randallholmes 3y ago
  It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
  - randallholmes 3y ago
    to the original poster, 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.

bmitc 3y ago

> Randall Holmes has claimed to have a proof of its consistency. In this repository, we use the interactive theorem prover Lean to verify the difficult part of his proof, thus proving that New Foundations is indeed consistent. 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".

Ericson2314 3y ago
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.
enricozb 3y ago
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 https://zeramorphic.github.io/con-nf-paper/main.l.pdf

Agingcoder 3y ago

I very much like this. I wonder whether this will eventually lead to collaborative proofs , and ‘ bug fixes’ , essentially turning maths into a process similar to code on GitHub.

trenchgun 3y ago
Already is. Check Lean blueprints. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
practal 3y ago
Yes, this idea of collaborative proofs has been around for a while now, at least for 10 years: https://arxiv.org/abs/1404.6186 https://arxiv.org/abs/1404.6186

randallholmes 3y ago

I would say that there is very little danger of a proof in Lean being incorrect. 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.

spindle 3y ago
Many congratulations on being formally proved right, Randall!
mckirk 3y ago
That's always the problem with these pesky computers. They do exactly what you tell them to.
sn41 3y ago
Congratulations on the verification of your proof! It must be great to have your research life's crowning work being formally confirmed! Also a great victory for the new foundations of Quine.
- randallholmes 3y ago
  I have shown the consistency of New Foundations. My aim is not actually to promote it as a working set theory. NFU, which admits Choice, is probably better for that. But if there are people who want to use NF as the foundation, it is now seen to be as secure as a rather small fragment of ZFC.
Strilanc 3y ago
Another danger is some sort of bug in Lean itself. This isn't unprecedented in theorem provers [1][2]. These might be hard to hit by accident... but there are larger and larger collaborations where arbitrarily people fill in steps (like [3]). Someone trolling one of these efforts by filling a step in using a bug they found might become worth worrying about. [1]: https://inutile.club/estatis/falso/ https://inutile.club/estatis/falso/ [2]: https://www.youtube.com/watch?v=sv97pXplxf0 https://www.youtube.com/watch?v=sv97pXplxf0 [3]: https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...

jraph 3y ago

I was wondering what were the fundamental differences between Coq and Lean and if they operated on the same kind of logic and found this [1]. 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-are-the-main-differences-between-coq-and-lean https://proofassistants.stackexchange.com/questions/153/what...

xvilka 3y ago
There are, you can check this discussion [1] as well. [1] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871