Hacker News Reader

Comment by anon-3988 | Hacker News Reader

The other crucial part to this is the ability to actually encode and test the theorem (via Lean). Otherwise, we would be swarmed with a billion lines of theorems that no one will be able to ever understand and verify anyway.

View on HN

A majority of these proofs have not been formally verified yet, I think people are overstating how important lean is to the success of LLMs in mathematics.

A paper and a lean proof are always going to be better than just a paper. I think mathematicians generally will not read AI math papers that haven't already been verified, especially since we're about to see a ton more AI math papers. Lean will remain important

Are there any AI generated proofs that are simple enough to be verified quickly by a human, that have not been lean verified? Or are they all basically incomprehensible?

The approximation of edit distance result [1] seems pretty readable to me, but the learn proof is still incomplete [2]. It's certainly much less readable than a good human written proof but it's certainly better than the last generation of AI proofs.

[1] https://github.com/openai/math/blob/main/preprints/An-Almost... [2] https://github.com/openai/math/blob/main/lean/ComparatorChal...

If you think AI-generated Lean proofs are unreadable, imagine Opus 5 generating informal proofs.

I think OP is saying Lean does indeed help.

whoosh

Opus 5 is ancient history now. Move on.

Yeah! They forgot to put a .5 after it! What an idiot! Just imagine if they would have written a 4!?!? We may have had to ban them from the website entirely.

The point both are making is that 5.5 produces readable output and 5 to a significant degree did not.

Reply on news.ycombinator.com