3 ms·
What if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or tre
by not-so-darkstar 28d 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 28d agothat'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 28d agoI 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.