Hacker News Reader

There are some parallels here to AI coding where even if the AI can write all the code, it's still valuable to have a human who can read and understand the code to verify correctness. The same is true of AI generated math proofs that humans will want to verify are around before they feed them back into the AI and build new insights.

View on HN

Proof verification can be done automatically via Lean (or similar), so the parallel breaks down unfortunately. The only thing humans really need to verify is the translation of the theorem statement and the correctness of the proof checker.

The purpose of having a human look at LLM output is not just to verify correctness but also to understand a system. The parallel to math is that the value of a proof is not just the verification of a statement but also the working out of the mathematics required to establish that truth.

Reply on news.ycombinator.com