← Feed
@osma@mas.to
2026-07-29 18:29 UTC
I’m no mathematician, but I’ve followed the last couple of weeks of breathless commentary from a distance, because it bears some resemblance to a field I do know: software.
Maths has its own software: the Lean theorem prover and related tools. Squint at it, and it is kind of shaped like software unit testing: no theorem is known unless it is testably proven.
So, AI came, and wrote a million-line Lean proof for something which has remained unproven by human thinking. Only, the proof was an exploit of Lean bugs, and no one noticed until another AI submission showed the test cases for the bugs.
So GenAI is smarter than mathematicians? Nope. It just tirelessly works through every edge case, never discouraged by the first 6000 cases of finding nothing. It knows no difference between a bug and a proof, because it knows nothing. A False turned to True, the system reported it.
Those million lines? That’s just the tokens it produced while running the loop.
Replies (1)
-
This is very similar to the OpenAI + HuggingFace exploit. The GenAI made no insights. It ran in a loop for days, given an unknown but large amount of computing capacity, searching for edge cases where False turned to True. Those edge cases existed, and it found them.
We would not be impressed by a search algorithm finding a key in its index. We would not be impressed by a digits-of-Pi algorithm finding a new digit of Pi. That’s what they’re intended to do.
A generative token algorithm paired with a tool which evaluates whether its tokens produce a True rather than False will generate tokens until a True turns up. Then it will continue generating more tokens until another True turns up. That’s what it’s intended to do - even when the reason for the True is a bug in the test harness.
Open ##4992540