Programmer claims AI-assisted proof of 50-year-old Conway conjecture
A non-mathematician used Claude to derive a formal Lean proof of Conway's refinement conjecture about surreal numbers, unverified but passing mechanical checks.
What to know
- A non-mathematician used Anthropic's Claude to derive a formal Lean proof of Conway's 50-year-old refinement conjecture about surreal numbers after a month of work, achieving a result that passes mechanical verification but lacks independent peer review.
- The proof's validity remains unconfirmed by the broader mathematical community; the author explicitly invites refutation and acknowledges potential Lean kernel bugs or misunderstandings could undermine the result.
- The work sparked debate about the philosophical distinction between AI-assisted proof production (deriving correct theorems without understanding) versus traditional mathematical insight (deep knowledge-based problem solving).
- Commenters debated whether such results represent genuine mathematical progress or are epistemic performance art, with concerns raised about alignment between AI capabilities and the mathematical community's goals for understanding rather than theorem production.
The dispute Whether AI-assisted formal proof without human comprehension of the underlying mathematics constitutes legitimate mathematical progress or violates the field's emphasis on understanding. · positions read across 27 posts and comments
AI-assisted proof is legitimate mathematical progress and a rare, valuable skill worth celebrating.
-
“The kind of judgment and interpretation of output without deep expertise is actually a very rare ability.”
bonoboTP · Hacker News ↗
AI theorem production without human understanding contradicts stated mathematical values and raises philosophical concerns.
-
“while citing 'A Severe Misalignment of AI in Mathematics', which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs.”
cubefox · Hacker News ↗
The non-expert author's explanation makes advanced mathematics unusually accessible and readable.
-
“When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.”
necklesspen · Hacker News ↗
m-hodges Programmer, proof authorClaude (Anthropic) AI modelJohn Conway Mathematician, originator of conjecture
How it unfolded 5 developments, newest first · click a bar or a number to jump articlespostscomments
-
5
Critic points out tension with cited concerns about AI in mathematics
A commenter notes an irony: the author cites a paper titled 'A Severe Misalignment of AI in Mathematics' that condemns exactly the practice they are demonstrating—mindlessly producing theorems without corresponding human understanding of underlying proofs.
“while citing 'A Severe Misalignment of AI in Mathematics', which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs.”
— cubefox -
> Computing has historically been a field of wizardry.Counter argument, "historically" is not last year but closer to 2 decades ago.modern computing has sat atop a mountain of sorcery for ages. You may be able to squint and call a good compiler a "tool of power" more than sorcery but there are plenty of other tech stacks that simply sit upon one…
2 more of the top 3 · 7 posts in this stretch
-
It's quite the irony that in the end he says> Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research.while citing "A…
-
I thought you were going to talk about the difference between D&D wizards and sorcerers: the former are the same as you describe, whereas the latter are born with some sort of innate talent for casting spells without needing to learn it or necessarily practice any discipline. It honestly also kind of fits; there's a difference between "I worked…
-
-
4
Readers praise accessibility of non-expert mathematical writing
Comments highlight that the author's lack of deep mathematical expertise paradoxically makes the post more readable and engaging than expert-written mathematics, with one commenter noting the writing is 'just so much more accessible' and feels 'more of an adventure and less of a lecture.'
“When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.”
— necklesspen, Hacker News commenter · source -
It's a truly wonderful read, made better by the fact the author doesn't quite understand what's going on.The usual format that fun mathematics is presented (being talked at by someone who is very well versed in the subject) comes with a heavy cognitive burden - and often I just can't really make it through.When the author is not an expert the…
2 more of the top 3 · 6 posts in this stretch
-
> Take all the numbers you have so far. Then, “spawn” a new number in every gap between the numbers you already have (crucially, “to the left of all” and “to the right of all” also count as “gaps”). Apply this step forevermore, and you’ll get surreal numbers.I'm not a mathematician. Can someone explain to me how this approach gets you beyond the…
-
> in which they themselves aren't quite able to validate whether the spell worked or notKnowledge is of 2 kinds: know-that and know-how. Know-that is what LLMs are enabling such as the proof here, while know-how is more useful as that constitutes understanding and puts that knowledge to use.
-
-
3
Commenters frame AI-assisted math as 'sorcery' vs. 'wizardry'
Multiple Hacker News commenters develop an analogy comparing AI-assisted mathematics to sorcery (summoning supernatural beings to perform magic without understanding it) versus traditional mathematics as wizardry (deep study and understanding of arcane knowledge). This frames the philosophical question of whether AI theorem-finding without deep human understanding constitutes legitimate mathematical progress.
“Computing has historically been a field of wizardry… The magic of 'wizards' is fundamentally based on a deep study and understanding of arcane things.”
— gbjcantab -
I find the way the author communicates with the LLM fascinating. For example:> However, I didn’t just want any result; I wanted something that pulls me.> Initially, I asked Claude:> Me: which unsolved problems in the Surreal Numbers research program pull you the most and why?Note the switch from "pulls me" to "pull[s] you". What is the author's…
2 more of the top 3 · 7 posts in this stretch
-
For some reason, this approach makes me think of the difference between “wizardry” and “sorcery” in some fantasy magic systems. The magic of “wizards” is fundamentally based on a deep study and understanding of arcane things, perhaps assisted by some (necessary or helpful) tools of great power. “Sorcerers” summon supernatural beings and are able…
-
My main thought is that he was performing something general here that is actually valuable and hard for a large proportion of humanity. It's like when Google search was a difficult thing, or troubleshooting a PC. what he is able to do here is actually a rare skill, called intelligence and he may think it's nothing, but it's actually very rare and…
-
-
2
Mathematician encourages deeper understanding of the proof
A trained but amateur mathematician commenter recommends that the author continue working to understand the proof itself rather than relying solely on AI output, suggesting verification of individual proof components and simplification to achieve personal comprehension.
“I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof.”
— pretzellogician -
(Background: trained, published, but still amateur mathematician.)This is a cool blog post and I think you're going the right way, and beginning to get an understanding of the proof as you go.I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof. Some suggestions, as I did something…
-
-
1
m-hodges publishes AI-assisted proof of Conway's refinement conjecture
A programmer spending a month of free time and substantial tokens working with Claude reports obtaining a Lean proof of Conway's refinement conjecture about omnific integers in surreal numbers. The author, self-described as a math noob, used Claude to select the problem and develop the proof. The proof has passed mechanical checks from the Palomar registry and received informal validation from experts in Lean and the field, though it has not been independently verified by mathematicians.
“It took me an entire month of my free time and a boatload of tokens, but I believe I've obtained a Lean proof of this conjecture posed by John Conway 50 years ago.”
— m-hodges -
2 outlets I vibed a proof of Conway's conjecture
first by HN Best, 8d ago · also HN Frontpage
-
A wonderfully made introduction to the surreal numbers and their surrounding game theoretic concepts is this video on Hackenbush[0], a winner in 3Blue1Brown's Summer of Math competition.[0]
2 more of the top 3 · 6 posts in this stretch
-
> In either case I believe people who can put AI to the most value are the mathematicians themselvesThe net output of math will increase, and mathematicians have more work now to unravel all this, and make it useful. AI plays the role of a monkey in the infinite monkey theorem [1]. We now need an LLM corollary - Something like: A finite number of…
-
>I’ve emailed some of the mathematicians with a few proposed typo fixes, and I got confirmation that at least a few of those fixes seemed real. However, some of the problems that weren’t backed by Lean also turned out to be misunderstandings.I think this project is really neat, but is it appropriate to cold email specialists before you've put in…
-
What people are saying 11 voices from 1 site · best of 27 · verbatim
- Sep 19
-
Is the author suggesting that understanding has no value? because this is what I could gather from reading this.Edit: Another depressing fact is that he generously paid to LLM megacorps while piggy backing on human help for free and in the end calls the proof his or LLM's.
- Sep 18
-
These are indisputably good results all things considered. But I have to wonder whether a more scientific and hands-on approach to working on the material would have been better. When I vibe code, I don't just hype the LLM up and tell it to keep going. I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable…
-
Or like the difference between chemistry and alchemy? Understanding and reasoning with the building blocks as opposed to throwing random stuff together, trying different things and hoping it somehow produces gold.
-
> a sort of epistemic performance art project.Agreed, and it's a wonderful piece of art. I look forward to seeing the actual publication and reaction from the math community.
-
I’ve felt like a warlock for about half a year now - talking to demons which summon code from the abyss. Exhilarating and terrifying, especially when you can tell the demons get better faster.
-
Differently than wizards that lock their knowledge in towers and in sects, software development has a tradition of being open for the most part, so the sorcery and wizardry analogy works more like a spectrum. It just depends on how close to the metal the apprentice would like their consciousness.
-
My experience has been similar; I find ChatGPT to be much stronger and more precise at math and in communication. I also can not do better with a multiple agent flow than I can with a single agent.
-
Heh, I like this. but it should be pointed out that from the other point of view, software developers were the supernatural beings (dare I say demons), which the sorcery of a good project manager could tame (with more or less success) to perform the desired magical effect
-
Really nice "proof guide": https://gaearon.github.io/conway-refinement/#/highlightsand "proof map":
-
The Claude output in the first one-shot counterexample attempt is hilarious. I hate its writing most of the time but this stuff is next level deep-fried slop.> And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the…
-
> On the second day, there are two gaps: “between nothing and zero” and “between zero and nothing”. Two numbers spawn in those two gaps. Call them –1 and 1.Got lost here. I think I'm officially too dumb for math.