[HN Gopher] New Foundations is consistent - a difficult mathemat...
___________________________________________________________________
New Foundations is consistent - a difficult mathematical proof
proved using Lean
Author : namanyayg
Score : 228 points
Date : 2024-04-23 12:01 UTC (10 hours ago)
(HTM) web link (leanprover-community.github.io)
(TXT) w3m dump (leanprover-community.github.io)
| _jcrossley wrote:
| 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 wrote:
| You could start with the Natural numbers game.
|
| https://adam.math.hhu.de/#/g/leanprover-community/NNG4
| gerdesj wrote:
| 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 wrote:
| Hope you keep going with it, it's a blast!
| gerdesj wrote:
| 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.
| _jcrossley wrote:
| Yea I've run through that a couple of years ago - was
| brilliant, had a lot of fun. But I mean to stay up to date
| and somehow contribute from the sidelines
| shepherdjerred wrote:
| Wow, that's actually really fun. Is this what "proofs" are in
| math classes?
| cwzwarich wrote:
| 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 wrote:
| 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 wrote:
| 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.
| ducttapecrown wrote:
| Kirti Joshi from the IAS has made very serious attempts to
| patch up Mochizuki's work by developing new math and by
| making the exposition good. If you're an expert in
| arithmetic geometry presumably he's readable, if you're
| just interested, I found it fun to skim.
| Davidzheng wrote:
| No comments on the correctness of his work (plenty of
| discussions online e.g on MO) but why do you say he's
| from IAS?
| nextaccountic wrote:
| There's a proposed proof of abc conjecture that is supposedly
| more readable. Here is a discussion thread about it:
|
| 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.
| barfbagginus wrote:
| I seriously doubt mochi's going to be any help for the lean
| formalization effort.
|
| But a lean-assistive llm trained on mochi's work? Ahhh! What
| an intriguing possibility!
| Chinjut wrote:
| I do not imagine LLMs will be of any use here.
| barfbagginus wrote:
| Then it's time to update your LLM reading!
|
| https://leandojo.org/ https://github.com/lean-
| dojo/LeanCopilot https://arxiv.org/abs/2404.07382
| Davidzheng wrote:
| These llm's are usually only proving some trivial lemmas
| right now. Hopefully it changes soon but...
| toneman wrote:
| I have studied IUT since 2012, and it is indeed, totally
| baroque. However, Motizuki Theory, is totally rebased and
| admits results of much interest. I will write more on this
| matter if my claim is of mutual interest.
|
| 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.
| hiker wrote:
| Liquid Tensor Experiment also comes to mind:
|
| https://www.nature.com/articles/d41586-021-01627-2
|
| https://leanprover-community.github.io/blog/posts/lte-final/
| Davidzheng wrote:
| Disagree. That one was not in question for years. Only Peter
| Scholze proved it and said he's not completely sure
| OscarCunningham wrote:
| It's a similar situation to the Kepler Conjecture
| (https://en.m.wikipedia.org/wiki/Kepler_conjecture). The proof
| was already known, but people weren't sure it was correct until
| it was formalised.
| xylol wrote:
| I'm really not from the field but wasn't there some Godel theorem
| showing every system strong enough cannot show its own
| consistency?
| peteradio wrote:
| 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 wrote:
| The system isn't being used to prove its own consistency. The
| consistency is proved in a different, stronger system.
| hyperpape wrote:
| Godel's incompleteness theorems are what you're thinking of.
| 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".
| skhunted wrote:
| 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.
| libeclipse wrote:
| It would tell you that the system is inconsistent
| skhunted wrote:
| It would not. If a system can prove (I know sufficiently
| rich systems can't do this but suppose it could) its own
| consistency you still can't conclude it is consistent.
|
| 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.
| roywiggins wrote:
| GP is (I think correctly) stating that a system that can
| "prove" its own consistency is _definitely_ inconsistent.
| Inconsistent systems can "prove" anything; if a system
| can appear to prove its own consistency, it isn't.
| skhunted wrote:
| Yes. I know this. What I'm saying is that even if a
| consistent system that was strong enough could prove it's
| consistency then it still wouldn't tell you anything.
| There are system that can prove their own consistency for
| which it is known that they are consistent.
|
| https://en.wikipedia.org/wiki/Self-verifying_theories
| francasso wrote:
| You should take this proof as saying: if Lean 4 is consistent
| then New Foundations is consistent. There is no contradiction
| of Godel's incompleteness theorem.
| einpoklum wrote:
| 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?
| Mathnerd314 wrote:
| I was just editing the Wikipedia article, it should be more
| readable now: 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 wrote:
| It's not magic: the universe of NF and other "big" objects in
| this system must be handled with extreme care.
| randallholmes wrote:
| 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.
| einpoklum wrote:
| So, is the article/project concerned with "just NF", or
| "NF with urelements"?
|
| Also, now I have to go learn about urelements too :-(
| randallholmes wrote:
| to clarify, when you look at objects that lead to paradox
| in naive set theory; they do not lead to paradox in NF or
| NFU; they exist but have unexpected properties.
| Mathnerd314 wrote:
| While you're around, I have a question: In TST, the
| restriction for x^m in y^n is that n = m+1, i.e. the level
| must increment by 1. In TTT, the restriction is instead
| that m < n, there is no requirement that it only be 1. Now,
| in NF, the restriction for set membership in stratified
| formulas is also +1. Is it possible to relax this to a
| "Tangled NF" where the set membership restriction is only
| that m < n? This would resolve issues such as how many
| levels it takes to construct an ordered pair.
| dwheeler wrote:
| I agree, a "cool" think about NF is the universal set.
|
| 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.
| dkbrk wrote:
| > 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
|
| 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.
| Smaug123 wrote:
| The thing I find really aesthetically pleasing about NF is how
| it adjusts the axiom of subset selection so that "the set of
| all sets" doesn't cause Russell's paradox. Basically it
| requires that the predicates you use to select subsets must
| obey a certain very lightweight type system. "x is not a member
| of itself" is not a well-typed question under any reasonable
| type system, and in particular it doesn't satisfy NF's
| "stratifiability" requirement, so you can't use it to construct
| the Russell's-paradox set of all sets which do not contain
| themselves.
| bmitc wrote:
| > 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".
| enricozb wrote:
| 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
| appplication wrote:
| 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.
| enricozb wrote:
| Such is the nature of math as well.
| appplication wrote:
| 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).
| golol wrote:
| 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.
| ChadNauseam wrote:
| 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).
| golol wrote:
| 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.
| enricozb wrote:
| 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.
| konstantinua00 wrote:
| 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
| bmitc wrote:
| 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.
| fwip wrote:
| 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?
| vilhelm_s wrote:
| 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.
| Certhas wrote:
| 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.
| cvoss wrote:
| 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.
| rowanG077 wrote:
| 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.
| dwheeler wrote:
| 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.
| agalunar wrote:
| For the curious: I assume the parent is referring to Pasch's
| axiom.
|
| https://math.stackexchange.com/questions/1901133/euclids-
| ele...
| dwheeler wrote:
| 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/metama
| th/set.mm/blob/develop/verifiers.md
| munchler wrote:
| > 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.
| Agingcoder wrote:
| 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 wrote:
| Already is. Check Lean blueprints.
| https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
| practal wrote:
| Yes, this idea of collaborative proofs has been around for a
| while now, at least for 10 years:
| https://arxiv.org/abs/1404.6186
| randallholmes wrote:
| 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.
| randallholmes wrote:
| The problem I express relates to the issues people mention
| about libraries: if a defined concept is used, one has to be
| sure the definition is correct (i.e., that the right thing has
| been 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.
| randallholmes wrote:
| and it very much IS an essential part of my confidence in
| this proof that conversations between me and Sky Wilshaw
| reveal that she understands my argument [and was able to
| point out errors and omissions in paper versions!]
|
| 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.
| pvg wrote:
| There's a (small, grey) link that reads 'edit' among the
| links at the top of each comment you can use if you want to
| change or add something to a comment you've already
| written, if you prefer that to replying to yourself.
| Smaug123 wrote:
| I am sure you know this, but for the audience: the danger can
| be mitigated somewhat with a "test suite" of theorems and
| examples about the definitions. These examples can be very
| simple ("this particular object, with this particular
| operation, is a group; this other object is not") or much
| more sweeping and general (e.g. fundamental theorems like
| "all objects with this property are isomorphic" or "all
| objects with this property embed canonically in this other
| construction"). It doesn't _prove_ that your definitions are
| correctly capturing what your natural-language proof talks
| about, but it can help you be more confident.
| btilly wrote:
| The paper makes a similar point like this:
|
| _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._
| amw-zero wrote:
| This is precisely why humans will always be involved with
| creating software.
| nathan_compton wrote:
| This doesn't seem to follow. Why kind computers get better
| at doing this (anticipating what humans want or whatever)
| than people? Some people are better at it than others and
| people are not magic, so I'd guess at some point computers
| will get it too.
| jpt4 wrote:
| > 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.
|
| 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.
| amw-zero wrote:
| This is why specification is much more important than
| verification / proof. We are bound by how accurate we make our
| propositions.
| jraph wrote:
| 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...
___________________________________________________________________
(page generated 2024-04-23 23:00 UTC)