Comment by flockonus
1 day ago
This clearly hit a nerve in very interesting ways!
Suppose we have a very convincing math PhD impersonator, agreeing and making some prepared smart-sounding comments saying they understood the proof and it seems to make sense - would it?
Well, most would say - NO! Obviously not, knowing this person was an impersonator. Others now knowing could be convinced of the validity.
Very simple thought exercise that allows to conclude, someone "saying they understood" (or agree) bears absolutely no weight to something's validity.
The idea that OpenAI's proofs are fake is contradicted by the response of mathematicians. Were they fake, mathematicians would not consider this release important enough to comment upon[1,2], as vixra always provided a steady supply of such writings. Nor would they be able to write expositions and simplifications, of which several are published each day on arxiv (just search OpenAI on arxiv to find them).
But perhaps mathematicians are no longer able to be the best judge if a proof is valid. Yet nobody but them is able to even understand what is claimed to have been resolved.
It is really strange to see mathematicians of the highest rank taking these results seriously[3], holding lectures explaining them, yet see it dismissed here as a mass psychosis. [1]https://smf.emath.fr/actualites-smf/20-10-26-communique-sur-... [2]https://www.mathsoc.jp/publicity/news20261016.html [3]https://terrytao.wordpress.com/2026/10/19/a-sketch-of-the-pr...
> But perhaps mathematicians are no longer able to be the best judge if a proof is valid
It seems they are still the best judge of whether a proof is useful or insightful though. AI is going to reward hack and try to eke out a win whatever it takes - which is fine if you regard these problems as trophies to be won, but not so fine if you take them in the spirit intended.
The famous problems that OpenAI (primarily) are trying to trophy-shoot with AI are famous because some human mathematician such as Erdos had the taste to judge them as fruitful grounds for new math to be developed in the pursuit.
Until we're at the point where AI is capable of things like creativity, curiosity and continual learning, AI will remain reliant on humans to fundamentally advance math and give it new tools to apply. For humans to do this it is helpful if they are inspired by the challenges set by their peers, which is why AI solving these human challenges is so counter productive - the snake is eating it's own tail.
> It seems they are still the best judge of whether a proof is useful or insightful though.
How can you be so sure of that? Like we know that human mathematicians can judge usefulness or insightfullnes. But we don't really know whether AI can do it even better. Like I don't think anyone has set up an evaluation of that.
> Were they fake, mathematicians would not consider this release important enough to comment upon[1,2], as vixra always provided a steady supply of such writings.
Few articles on vixra are made by companies with ~$1T valuations.
The truth is still tying it's shoes, in that metaphor.
Analysing all the proofs and finding contradictions or not takes time.
> But perhaps mathematicians are no longer able to be the best judge if a proof is valid.
Not the way they're written, and not at the rate they're dumped on the math community, at least.
[dead]
> Very simple thought exercise that allows to conclude, someone "saying they understood" (or agree) bears absolutely no weight to something's validity.
Well, it is always was so? It doesn't matter if the person claiming things is impersonator or not, either you dive into the topic yourself and decide for yourself, or you wait for a consensus among specialists to settle.
I mean, in 2026, after the rise of the Internet, where lies are widespread, AND after the rise of an AI, that removed such anchors of truth as a video proof for example, I believe everyone smart spend some time meditation on an operational definition of truth and now has something that doesn't depend on knowledge that the source is not an impersonator.
Yeah from an objective truth seeking perspective, and i agree with you, it's hard and often times impractical.
About 2y ago, before AI was all the rage - lookup: controversy, scientific fraud networks, "paper mills"
Now imagine that PhD “impersonator” has, in the past few months, made more demonstrable progress in mathematics than anyone in history.
I think that would change the conclusion of the argument a little.
Or maybe the PhD impersonator discovered a soundness bug in a component of Lean and was able to exploit it.
With no humans able to understand the proofs the impersonator has produced, there's no way of knowing.
There are many independent implementations of Lean's proof checker:
https://arena.lean-lang.org/
It's highly implausible that the same bug is present in all of them.
4 replies →
If the AI had found a bug, I expect it using the bug to prove everithing and geting 700 pdf per week https://xkcd.com/704/
This is true of literally any proof of sufficient complexity, human-authored or otherwise.
It takes time to convey the core ideas. It takes time for other mathematicians to come up to speed on the new techniques and approaches or the novel combinations of existing ones.
The actual experts in this field have asked for the argument to be explained to them, and are now at the point where they believe this is plausible. Another person in this thread has produced a Lean proof and presumably is not trying to pull a fast one on us by exploiting a bug in the solver.
TL;DR chill bro.
More realistically, that impersonator has created lots of output, and the correct ones are selectively publicized (and few particularly interesting bad answers).
Yes from a social proof perspective.. not really from an objective truth seeking perspective, the best liar tell truths 99% of the time.
Do you really believe Open AI made more progress in math than any of the human predecessors? Come on.
Galois had built modern algebra before dying at 20. What agents did so far is flash in a pan.
Wait and see when _they_ are 20 years old!
1 reply →
He should have written longer letters and duelled less.
> Galois had built modern algebra before dying at 20.
No he hadn’t. You are clearly consuming mathematics through a pop culture lens.
1 reply →
The recent progress does not imply that the "impersonator" has a deep understanding of mathematics. By formalizing a problem in Lean, constructing the proof is essentially a complex search. Because Lean is the arbitrator of correctness, the "impersonator" can make as many mistakes as they want until they find a solution that passes the checker. That is very different from checking a paper for correctness.
complex searches are quite valuable in mathematics. For example, Maryna Viazovska's fields medal was for finding the right gadget (roughly, a complex search) to prove optimality results in sphere packings.
1 reply →
that's a hard cope. You think humans don't make thousands of mistakes to come up with something good?
1 reply →
Good luck writing a Lean proof of a nontrivial theorem by giving a keyboard to a thousand coke-fueled monkeys. If only it was that easy.
4 replies →