6 ms·
I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
by DoctorOetker 11d ago
I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
- fspeech 11d agoI don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-frey-package-wlog.md https://github.com/htzh/flt_for_human/blob/main/math/001-fre... which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
- DoctorOetker 10d agoI don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages). The Lean system has already experienced soundness bugs. The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this. I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
- fspeech 10d agoProofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.