6 ms·

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type.

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct

gorgolo 1mo ago
> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?
- SkidanovAlex 1mo ago
  It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct. This is how the theorem for FLT looks in the particular proof we discuss here: theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct. This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof. (Not impossible: such a bug indeed was recently discovered (and patched))
  - YeGoblynQueenne 1mo ago
    Couldn't the kernels have different bugs?
  - thejokeisonme 1mo ago
    You emphasize TWO as of these kernels are so different.
- aureianimus 1mo ago
  There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.
- raincole 1mo ago
  If you just "translate" an existing proof step by step to Lean, then of course you could mis-encode the intermediate statements too. But if you mis-encode the steps and still pass Lean check, it means you found a new proof! (Or you found a bug in Lean)
thrance 1mo ago
And (3) the axioms are correctly encoded too.
not-so-darkstar 1mo ago
What if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?
- robotpepi 1mo ago
  that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.
  - not-so-darkstar 1mo ago
    I think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.

gorgolo 1mo ago

> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?

SkidanovAlex 1mo ago
It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct. This is how the theorem for FLT looks in the particular proof we discuss here: theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct. This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof. (Not impossible: such a bug indeed was recently discovered (and patched))
- YeGoblynQueenne 1mo ago
  Couldn't the kernels have different bugs?
- thejokeisonme 1mo ago
  You emphasize TWO as of these kernels are so different.
aureianimus 1mo ago
There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.
raincole 1mo ago
If you just "translate" an existing proof step by step to Lean, then of course you could mis-encode the intermediate statements too. But if you mis-encode the steps and still pass Lean check, it means you found a new proof! (Or you found a bug in Lean)

thrance 1mo ago

And (3) the axioms are correctly encoded too.

not-so-darkstar 1mo ago

What if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?

robotpepi 1mo ago
that's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.
- not-so-darkstar 1mo ago
  I think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.