4 ms·

To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't

by fspeech 28d ago

To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.

fspeech 28d ago
The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main/tools/docs-site/README.md https://github.com/anthropics/fermats-last-theorem/blob/main...
- DoctorOetker 28d ago
  I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
  - fspeech 28d ago
    I 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 27d ago
      I 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 26d ago
        Proofs 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.

by fspeech 28d ago

fspeech 28d ago

The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main/tools/docs-site/README.md https://github.com/anthropics/fermats-last-theorem/blob/main...

DoctorOetker 28d ago
I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
- fspeech 28d ago
  I 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 27d ago
    I 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 26d ago
      Proofs 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.