Hacker News Reader

Comment by tarsierscripter | Hacker News Reader

That’s of no use to anyone. Haven’t you been following this story? The value of a pure math proof is the understanding it brings and the additional questions raised along the way. Its truth value is of minor consequence.

That’s like skipping to the end of an important novel and thinking you got something out of it.

View on HN

I've been following the story. Git repos of Lean code are a good start to developing understanding. First verify that the proof is correct, then work on ways to simplify it and make it understandable.

Many of the proofs released by Open AI don’t have Lean proofs. Their system doesn’t work in Lean directly, it writes proofs in natural language first. Later, some of the proofs were passed through an auto-formalization model to generate Lean code which then passed Lean’s checks.

The issue is that the auto-formalization step itself is not trivial. There is no formal verification which proves the translation correct, so it is up to mathematicians to hand-check the formalization to make sure it’s saying the same thing. Unfortunately, this problem is undecidable in general.

We’ve already had a paper showing that auto-formalization can’t be trusted implicitly [1], so a GitHub repo of a bunch of Lean code can’t be trusted to prove what the title claims is being proved.

[1] https://arxiv.org/abs/2610.08144

> That’s like skipping to the end of an important novel and thinking you got something out of it.

Wasn't it just a few years ago that there were all sorts of apps ("Blinkist" ?) being pushed hard that did just that: give you the TLDR on some publication so that you could pretend to have read & understood it?

Reply on news.ycombinator.com