To ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true?
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
Formalizing Fermat's Last Theorem
51–60 of 523 posts
Re: Formalizing Fermat's Last Theorem
#52On a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)
100% It is a very insightful book
Re: Formalizing Fermat's Last Theorem
#53Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.
Note to other users: don’t downvote this kind of comment, answer it.
Re: Formalizing Fermat's Last Theorem
#54Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
The nice thing about theorem provers is that you don't need to read the intermediate lines. You need to make sure that the goal/result actually matches what you think it says - but everything in the middle is validated by the prover.
Re: Formalizing Fermat's Last Theorem
#55Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye: https://news.ycombinator.com/item?id=49203626 It is truly saddening to think that machines will deprive us of this wonder and experience. But truly exciting to dream about what lies beyond the limits of our biology.
> It is truly saddening to think that machines will deprive us of this wonder and experience.
It won't deprive us.
Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art:
Re: Formalizing Fermat's Last Theorem
#56So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?
Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.
If they’re asking that kind of question, do you think this answer will help them understand anything?
Re: Formalizing Fermat's Last Theorem
#57Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
Re: Formalizing Fermat's Last Theorem
#58Now /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?
Yes. FLT follows from the fact that you can't build the equivalent representation of n-simplex turning into a hypercube in dimensions higher than 2
/s
Re: Formalizing Fermat's Last Theorem
#59> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
There is no way Fermat could have fit that in the margin. Definitely vindicated.
Re: Formalizing Fermat's Last Theorem
#60Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.
So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.