Dan Abramov — a React maintainer, and by his own description a math noob — wanted to find out whether he could point a frontier model at an open problem and have it solved. A month of free time and roughly 40 billion tokens later he had a proof of Conway’s refinement conjecture, checked by Lean, plus a careful account of everything that went wrong on the way. It has not been independently verified by mathematicians, and he invites refutation.

What the problem is, in plain terms:

  • Conway’s surreal numbers are a number system containing the ordinary reals plus infinitely large and infinitely small quantities. The “omnific integers” are its integer part.
  • The conjecture, from 1976, is that those integers keep a property ordinary integers have. If 10 x 21 = 6 x 35, that equality is really four numbers reshuffled: (2 x 5) x (3 x 7) = (2 x 3) x (5 x 7). Conway believed every such equality among omnific integers can be reshuffled the same way.
  • Lean is a proof assistant: it machine-checks every step, so a proof either compiles or it doesn’t. It certifies the argument for the statement as written — it says nothing about whether the statement is interesting.

The setup that eventually worked

  • Roles, not one chatbot: a “PM” agent driving toward the goal and merging work, math agents hunting for results, a “red” agent whose only job was breaking other agents’ proofs, a “random” explorer, and a Lean agent formalizing whatever survived. Codex’s recurring “goals” reminders and inter-agent messaging kept the sessions from drifting.
  • Requiring Lean certification before stacking new claims — and testing the models against published literature first. They found real typos in a paper he depended on, which the paper’s authors confirmed, giving him a way to tell whether the models were hallucinating.
  • Burning everything down, twice. The pile of machine-written “papers” reached about thirty, where a single mistake invalidates everything built on top. Both teardowns refocused the project on the parts that were actually real.
  • Making the result legible: standalone statement files capped at a few hundred lines that import nothing but the standard library, plus proof maps so the model could see the shape of what it had built. The lesson he draws: a model can’t simplify what it can’t see, and can’t ignore terminology you leave lying around.

The failure modes worth knowing about

  • One-shot prompting produced word salad. His example: “The den has air in it. Drift fuel exists.”
  • Claude would certify results, then find flaws in work already merged, then “repair” them and find further flaws.
  • One markdown argument grew past 22,000 lines while its two decisive steps were still prose hypotheses.
  • “Untransferred obligations” turned out to be a euphemism for claims the model had not proven. Pressed on it, the model said so plainly.
  • Cost: around 40 billion tokens, roughly 210 million of them output, over 95% cache reads — an estimated $40,000 at API pricing, which he thinks better steering would have cut by 5-10x.

His answer to his own question — can this be done with AI alone — is yes, and no, and yes. The proof exists and he does not understand it; the models kept failing to structure the work; and the job he actually did, poking agents and noticing when they spiralled, could probably be handed to an agent trained to manage other agents. The dependable shape, as he describes it: a clear goal, a tentative direction, dependencies already machine-checked, and the mathematical agents only slightly ahead of what has been verified — close enough that the whole thing can’t become a house of cards.

What the thread adds

The 171-comment thread on Hacker News is substantive for a math post: a computability objection, concrete advice from a published amateur mathematician, and a live disagreement about whether “no understanding” is a result at all.

  • srcreigh — argues for a hard ceiling. No finite number of LLM agents can eventually find all theorems, since “this would imply that the busy beaver sequence is computable which implies the halting problem is decidable.” A human prompting the model adds an outside information source, which is the only thing that removes the limit.
  • gbjcantab — the frame that stuck for a lot of readers, wizards versus sorcerers: “Computing has historically been a field of wizardry. It’s… interesting (?) to see so many people pushing so hard in the direction of sorcery, and in fact applying that sorcery to other fields, in which they themselves aren’t quite able to validate whether the spell worked or not.”
  • pretzellogician — a trained, published amateur mathematician who has done something similar, with the practical next steps: check whether each part of the proof already exists in the literature and attribute it, merge redundant patterns, have the model referee the work like a journal reviewer, and keep simplifying until “you yourself can follow the proof.”
  • zozbot234 — reports (their word: “reportedly”) that the author has been in contact with Prof. Mantova, co-author of the human-made results the proof leans on, so a conventional publication may follow — while noting the AI-written version is “way too obscure for that.”
  • sigmar — the objection about norms: is it appropriate to cold-email specialists with proposed typo fixes before you can describe yourself as more than an amateur, when millions of people now use these tools to wade into new fields? The author replies that he waited until he was highly confident the errors were real and kept the messages apologetic and brief; vessenes counters that “if there are real errors in published work, I think most mathematicians want to know about them.”
  • msteffen — reads the post against Timothy Gowers’ spectrum of mathematical motivation and calls it “the ultimate meta-experiment of seriously undertaking a project that is intentionally 100% problem-solving and 0% understanding.” omnicognate disagrees with where that lands: the author can’t verify his own result, “has to lean on those who do have the understanding,” and can only call it likely — so “problem solving is as dependent on understanding as ever.”
  • nphardon — practitioner corroboration from another direction: they find ChatGPT more precise at math than the alternatives, and got nothing out of a multi-agent flow that a single agent didn’t already give them.

The question the post leaves open

FiatLuxDave asks what the write-up never answers: models are now proving conjectures, so where do the next conjectures come from, and has anyone had an LLM produce a conjecture at Conway’s level? The replies are opinion only, and the thread resolves nothing. It is a fair gap to sit with, because the project started the same way — the model chose what it found interesting.

Thread caveats: HN handles are pseudonymous and the site publishes no per-comment scores, so the ordering is HN’s own ranking rather than a vote. This is a slice of a 171-comment thread, not a consensus.