Re:Why the Legendary Erdős Problems Are Falling to AI
by eru on Wednesday August 05, 2026 @10:15AM
(#49183249)
That's why OpenAI also published machine-checkable proofs.
The process is very, very faintly similar to running a typechecker over your software sources.
Re:Why the Legendary Erdős Problems Are Falling to AI
by parineum on Wednesday August 05, 2026 @10:51AM
(#49183817)
They're publishing machine checkable proofs because that's the only way they, themselves, can check them.
They don't understand the math either.
Re:Why the Legendary Erdős Problems Are Falling to AI
by inigyou on Wednesday August 05, 2026 @12:07PM
(#49184781)
For 3.5 days we had a machine checkable proof the Collatz conjecture was false. There turned out to be a bug in the machine checker.
Re:Why the Legendary Erdős Problems Are Falling to AI
by eru on Wednesday August 05, 2026 @02:59PM
(#49187369)
Yes, however any LLM agent you asked about that proof could tell you that. (And even most humans who know a little bit about the bug.)
You are right that Lean isn't great in this respect, and people are working on proof formalisations that are less prone to bugs.
I can't tell if xkcd #435 is still true, or if math is just as mushy as everything else seems to be. When a math proof can only be understood by a handful of people, what does that mean about that proof? I think the LLMs are pushing a problem that existed already and pushing it further.
[0] https://xkcd.com/435/