Hacker News Reader

Comment by lseplot | Hacker News Reader

https://github.com/anthropics/fermats-last-theorem/blob/main...

  status: "self-assessed"

13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack.

Fable, please translate to HOL-light. Make no mistakes. You are doing great!

View on HN

It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.

We have a significant case split here:

A human mathematician writes a Lean proof:

- Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases.

An AI writes a Lean proof:

- AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.

Reply on news.ycombinator.com