Hacker News Reader

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...

View on HN

I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.

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-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.

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.

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.

Reply on news.ycombinator.com