AI Models Autoformalize Erdős Counterexample in Lean, Generating 1.2 Million Lines of Code in Three Weeks

Human mathematicians have been getting out-counterexampled for decades already. The real difference now is compute plus it being trendy, and the counterexample sizes we're seeing are about what pre-generative-AI search systems could already find.

The catch is that the same model doing this math can also write poetry and code your backend. It's not a narrow expert system trained just for this, that's why people are freaking out.

Mathematicians have used computers for over 50 years by bounding the problem first then brute forcing cases. AI is now doing the bounding step too, but humans still craft the prompts and know where to look, the search space is way too big for random trial.

Someone posted an actual reproduction prompt online (aaronlou.com link), and it's pretty generic, no explicit mention of reducing search space. So maybe modern LLMs really are figuring out the cleverness on their own.

I don't buy that it was just a casual prompt. This smells like a professional mathematician doing sustained work with LLM help plus an optimized numerical search running on a real compute cluster, not some ad hoc Claude Code session.

Disproving stuff fast is genuinely good, it saves people from wasting years proving something false and lets the field move to other questions faster.

Counterexamples are unsatisfying though. They give you an answer but not the understanding of why, and as long as humans judge what counts as an elegant or illuminating proof there's still work for us.

If AI ever finds a counterexample to the Hodge conjecture that would be enormous, it's a Millennium Prize problem. The autoformalization of the Golod-Shafarevich theorem mentioned in the post is already wild on its own.

That Hodge conjecture line from the author (Kevin Buzzard) reads like he's being tongue in cheek. A candidate counterexample alone wouldn't resolve it, you'd still need to prove no algebraic cycle or invariant subspace exists, much harder than just finding an object.

Reminds me of Yitang Zhang, who spent 7 years on the Jacobian conjecture and got burned when a corollary his thesis relied on turned out wrong, tanking his career for years before his twin primes breakthrough. Makes you wonder what would've happened if he'd had ChatGPT in 1986.

My own math research experience: I'm constantly surprised how many published assertions turn out false, and even propagated into applied literature, with a lot of defensiveness when you point it out. LLMs help but they're also confidently wrong a lot, like having a second person with different hunches.