News for hackers. Stuff that matters.

A comment on Why the Legendary Erdős Problems Are Falling to AI. Parent comment

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.
[ Parent | on HN ]
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.

[ Parent | on HN ]