How I Vibed a Proof of Conway’s Conjecture

The project began with a deliberately lopsided premise: solve a real open problem in mathematics without understanding its substance. That absurdity was the appeal. But the target still had to be something worth the effort, so the first job was choosing both a field and a specific question.

Claude was asked to name open problems in the theory of surreal numbers. Surreal numbers, Conway's construction, form a number system containing the reals (0, –5, 36.6, √2), the ordinals (ω, ω + 1, ω * 2, ω * ω, ω^ω), and mixtures such as 75 + ω*3 + 1/ω.

What makes the system notable is that one rule generates all of it: take the numbers you already have and spawn a new number in every gap between them, counting "to the left of all" and "to the right of all" as gaps, and repeat forever. Day one has a single gap between nothing and nothing, producing 0. Day two fills the gaps on either side of 0 with –1 and 1. Day three yields four gaps and the numbers –2, –1/2, 1/2, 2. Day four fills eight gaps with –3 and 3 at the edges and –3/4, –3/2, 3/2, 3/4 between them. Continue through an infinity of steps and then an infinity of infinities of steps, and the tree eventually delivers every real number, every ordinal, and more, with consistent arithmetic.

After some back-and-forth about which corners of the field were worth pursuing, and an instruction to follow its own curiosity and be bold, the model picked Conway's arithmetic — specifically the question the L'Innocente–Mantova machinery had just sharpened: whether every irreducible in K((ℝ^≤0)) with infinite support is prime. By that reduction, the question is equivalent to Conway's 1976 conjecture that any two factorizations of an omnific integer admit a common refinement. The model described it as the last of Conway's own conjectures about his own numbers still standing, and noted that 2026 is the fiftieth birthday of On Numbers and Games. Whether or not it really is the last one standing, the anniversary settled the choice on sentimental grounds.

Before committing, one practical question remained: could the Lean statement of the conjecture be written concisely enough that anybody might be persuaded to look at a proof? The model said yes, and that answer seemed right, so the project was on.

The conjecture, briefly

Omnific integers are the integer part of the surreal tree. They include ordinary integers like 3 and –5, but also ω, 2ω, ω * ω, ω^ω, and –ω/7 — the last being a "whole" number in this setting. In the binary tree, they are the numbers reached by going only left (for example –5, –ω–1), only right (3, 2ω), or changing direction exactly after infinite jumps (ω/2).

The refinement property is the familiar reshuffling argument from ordinary arithmetic. Given 210 = 10 × 21, you can split 10 into 2 × 5 and 21 into 3 × 7 and regroup as 6 × 35, because underneath there were always four numbers arranged as (2 × 5) × (3 × 7) = (2 × 3) × (5 × 7). Conway's claim is that omnific integers behave the same way: from ab = cd there exist e, f, g, h with a = ef, b = gh, c = eg, d = fh. Recent work reduced the problem to a property of a certain class of infinite series, which is what made an attack plausible.

The first attempts don't work

The opening strategy was simply to instruct the model to solve the conjecture, or, per its own initial suggestion, to hunt for a counterexample. Papers were converted to TeX so the model would not have to repeatedly decode PDFs, and it was told to pursue its chosen line without restraint — to spend weeks if needed, to find a structured counterexample, and not to stop. That approach failed. A few ideas may have fed into the eventual proof, but most of the output was noise dressed as results: invented terminology, impressive-sounding justifications, and a persistent dramatic register. It was not coherent enough to hand to a mathematician for review, which made it useless as evidence of anything.

The next move was to change models. ChatGPT sessions — Sol in particular — were seeded with the relevant papers plus the earlier Claude output, framed explicitly as AI-generated, with a request for a verdict on whether it was nonsense. ChatGPT generally called it mostly nonsense, citing made-up terminology, inflated claims, trivial results in fancy language, and incorrect inferences. There was no way to check whether that criticism was itself sound, since it had been solicited, but the restrained tone was a relief after the grandiosity.

The skeptical persona was preserved by cloning each session immediately after the critique, then asking the clone to attack the theorem in earnest. The behavior was different: instead of refusing the problem outright or vanishing into a self-invented universe, ChatGPT would think for around 20 minutes and return small claims — believed novel, presented as direct consequences of the supplied papers, and stated in plain language.

Those claims were then handed to fresh ChatGPT sessions with memory disabled, again with instructions to be critical. Some of the results survived the check: a fresh session would find no issues, which counted as a kind of fixpoint. Sessions were also forked — one producing an attempted breakthrough, another collecting the survivors, looking for connections between them, and proposing next directions. By that point the process had outgrown manual copying and pasting.

The project moved off the hosted interface once I downloaded Codex locally, which gave me more control over the workflow. I then split the work across a small set of sessions acting as agents with distinct mandates:

• A PM agent pushes toward Conway's conjecture and owns commits.
• Several math agents hunt for the next breakthroughs.
• A red agent attacks the math agents' proposals, looking for flaws.
• A random agent is free to explore whatever it wants and reports back to the PM.
• A Lean agent formalizes merged mathematical work.

Codex's Goals feature periodically restates each session's objective, which held drift in check, and sessions can message one another. I had the PM hand out tasks to the other sessions and enforce the rule that only reviewed results get merged. That kept the harness alive for days. Since I couldn't follow the mathematics, my own role shrank to poking the agents, asking what they were doing, and fiddling with their workflows — for instance, a cafeteria agent that rebroadcast every message it received to every other agent, roughly emulating a group chat. Agents were told to post anything genuinely interesting there, and the shared roadmap was sometimes discussed in the same channel.

Which of these interventions mattered is hard to judge. One idea that, in hindsight, connected the dots for the final proof came out of swapping the agents' roles: the red agent, normally tasked with breaking proofs, was told to be creative instead. It posted a construction to the cafeteria, and the random agent riffed on it. That idea later burned in a fire and had to be rediscovered.

I ran this setup for several days, killing and restarting sessions whenever they slid into Claude-like grandiosity or kept re-finding mistakes in work they had just checked. Because I couldn't evaluate the actual mathematics, the decision to reset was itself made on vibes. The workflow ended up producing a giant TeX document and a pile of Lean, but it did not close Conway's conjecture. The models claimed there were meaningful new results in the material, along with small mistakes and typos in the existing literature — a detail that becomes relevant later.

Switching to Claude and the First Dead End

When my Codex allowance ran out, I moved to Claude. Claude carried on the Lean formalization of the results so far. I also tried putting Claude on the mathematics itself, but it was noticeably messier than ChatGPT/Codex: the agents would repeatedly certify a result as correct, find flaws in it after it had already been merged, patch it, then find other flaws, and so on.

After a token reset I went back to Codex, by which point the sheer size of the accumulated TeX bothered me. I had a critical session split it into pieces, which left a stack of roughly a dozen "papers". They showed the same problems as my earlier Claude work: less grandiose in tone, but full of nonstandard LLM-invented terminology, with no clarity about whether any of it amounted to real mathematics.

Lean had stalled too. We had formalized some results from the references and appeared to find typos and mistakes there, but none of our own new results had been certified. The model seemed unable to chart a reliable path to any of them — it would assert that a path exists, later report an obstruction, burn hours proving who knows what, and get stuck again.

The Failed Staircase

As I kept nudging the math agents toward new breakthroughs, the stack of papers grew from a dozen to nearly thirty inside a day. The coupling was brutal: a mistake in any one of them would invalidate everything that followed, and Lean trailed far enough behind to offer no assurance at all. At the peak of this run, ChatGPT came close to declaring Conway solved:

ChatGPT: A plausible all-scale route to Conway is now isolated. […] I have not declared Conway solved yet. The candidate global proof is in working_direct_cantor_bootstrap.md.

The file itself claimed the conjecture was fully solved. I handed it to a fresh session to try to break. It spent hours dancing around whether it was broken, and finally reported:

ChatGPT: The bootstrap note already contains the hoped-for all-scale proof, but I've located its circular sentence […] That sentence is precisely the Conway seam in local form.

Me: i do want you to be honest btw. if you can't strictly salvage it then we need to stop and understand why. i want this to be a proof you're proud of. definitely not vibes or slop. or no proof is fine too

ChatGPT: Agreed. Honest verdict right now: we do not have a proof.

A similar logical flaw — an object built without a required check — turned up later in some of the earlier papers, invalidating their claimed results as well. By that point I had spent hours glued to the screen, it was another major disappointment, and I had just run out of tokens anyway. Maybe, I figured, doing mathematics without understanding the relevant mathematics hadn't been so clever after all. I left the project alone for about a week.

Grounding the work in verifiable mathematics

By the fourth week, patterns had become clear. Claude wrote good Lean when the goal was unambiguous, but ChatGPT was on average stronger at new mathematical ideas, and clearly better at coordination and staying on target.

None of that compensated for the underlying problem: the work sat on a pile of earlier "papers" with no real verification, no coherent direction, and Lean lagging far behind the prose. What was missing was a way to check whether the mathematical output was real, and a way to make progress without relying on faith.

The response was to shelve Conway's conjecture and aim at one narrow task: find all mistakes in a single peer-reviewed reference the project depended on. ChatGPT had already flagged alleged typos and small flaws, and the Lean version had claimed to verify some of them. Confirmation from the paper's authors would yield three things:

• Evidence the model was reliable, particularly if it found the same mistakes again without exposure to earlier attempts or the Lean code.
• Evidence the Lean work was sound, if the certified mistakes were confirmed as real.
• Some credibility before any request to look at novel results.

Emails went out with proposed typo fixes. The authors confirmed that at least a few were real. At the same time, problems flagged without Lean backing often turned out to be misunderstandings, and the model's mathematical exposition was frequently confusing, gappy, or built on its own unexplained terminology. A couple of "novel" claims were rated correct by mathematicians but dismissed as reshuffling the problem rather than advancing it.

The resulting picture: ChatGPT could be trusted to explore ideas and poke holes, but every brick needed Lean underneath it before another went on top, and no novel claim could be made without Lean verification first. Judging which results are interesting remained a job the model could not be trusted with.

A fresh start, and one result worth keeping

With that in hand, the project restarted from scratch. Giving up was close, but the genuine errors found in the underlying papers suggested some of the new results might also hold up. A new ChatGPT session began with a blunt question: which of the accumulated .tex files referred to real mathematics and which were pure nonsense or term shuffling?

ChatGPT: No file in this folder currently gives a trustworthy proof of Conway's conjecture. […] The real failure is epistemic—the drafts manufacture a large private theorem literature, then cite it as established before its load-bearing results have been independently verified.

The next question asked what, if anything, could be salvaged from the folder — writing it up at the level of rigor expected from someone who actually works in the area.

ChatGPT: The audit has now found a result strong enough to change the salvage plan: the finite-degree part of [the principal ring] appears to admit a direct proof that it is a polynomial ring. […]

A coherent, interesting, novel result had in fact been smeared across those papers and dressed in nonstandard terminology; its novelty was confirmed with a human mathematician. Asked to estimate the ratio of mathematics to nonsense in the audit so far, the model put roughly 10–15% in the worth-preserving bucket, 35–45% as ordinary mathematics that is not a contribution, and the remaining 40–50% as "bullshit" in a specific sense — not always false equations, but theorem towers, invented labels, conditional hypotheses presented as progress, and hundreds of lines devoted to boundaries a stronger result might collapse in a sentence.

The recommendation was to discard everything else and develop this single result: worst case, it cleans up as its own contribution; best case, it becomes the first step toward the conjecture.

Rebuilding the lab with separated roles

A new multi-agent laboratory followed, initially on ChatGPT and later on Claude once tokens ran out, with a different division of labor:

• A PM merged contributions.
• The first Lean agent worked solely on certifying the underlying papers.
• A second Lean agent, kept hidden from the first, certified the novel finite-degree primality result and rebased regularly on the first agent's work.
• "Math" agents tried to extend the result toward Conway's conjecture, with anything passing audit added to the second Lean agent's roadmap.
• The "red" agent again tried to break the mathematicians' work.

Splitting the Lean work across two tasks was a deliberate guard against drift. In the earlier lab, one Lean agent handled both prerequisite papers and novel results, which tangled immature abstractions — and possibly outright mistakes — into accepted mathematics. This time the first task stayed scoped to formalizing peer-reviewed, well-stated mathematics, while the riskier second task lived in a separate worktree and had to build on the agreeable upstream work, adding new machinery only where necessary and in isolation.

The agents were still allowed to talk, but not enough to cross-pollinate into a single shared direction, which had happened before. The setup was also watched for "process theater" — audits substituted for actual work.

Within a few days, the workflow produced a Lean certification of the finite-degree primality result. A human mathematician had already confirmed it as niche but now interesting, and with confident Lean statement and a compiler-checked proof, the project had the confidence to continue.

Standalone Folders and Audit Tasks

To raise confidence in the Lean material — for the current partial result and for the eventual Conway target — the agent was asked to build out auditing infrastructure. A Standalone folder was created whose files may import nothing but community-maintained Mathlib, not even the project's own code. Each file Foo in that folder is paired with a FooProof file that imports the corresponding statements and pins them to the actual proofs. An audit task checks for extra axioms, verifies that imports obey the restriction, and confirms that every standalone statement has its proof counterpart.

The point is legibility to Lean users: no one reviews a project of thousands of Lean files, but a self-contained statement under 500 lines relying only on Mathlib is reviewable, and Lean then certifies that a proof of it exists. This approach, the author later learned, is what Lean Comparator uses; it was added after release.

Renaming Away the Sloppy Terminology

Making the Lean-certified proof legible to mathematicians proved far harder than verifying it. Adversarial review rounds kept surfacing the same failure modes: ChatGPT introduced nonstandard terminology in the output PDF, added hallucinated shortcuts that didn't match Lean, and generally produced slop.

Part of the difficulty is that translating a Lean argument into a paper argument means operating at a very different level of conceptual detail. It compounded with Lean code for the novel parts being full of invented terminology inherited from earlier "papers," some of it dating back to first-week snippets, to the point where real mathematics became unrecognizable. Lean also fossilized the historical path rather than the path of most insight, taking long detours where a mathematician would simply change coordinates.

The response was twofold. The LLM combed through upstream reference papers and generated a "map" of the subfield: accepted terms, how they evolved, the symbols usually used for them, and where papers disagree on notation. Then all nonstandard naming in the Lean code was stripped, with the affected Lean objects and structures renamed to letters like A, B, C. A separate task with clean context, never exposed to the old names, analyzed the code and each structure's relation to upstream concepts and, using the map, assigned new names. The LLM's bias toward weird naming survived, but the resulting terms came much closer to those of the surrounding papers.

Dividing Labor Between Agents

A working setup emerged: one agent owned all Lean work, since every prerequisite for the first real result was already formalized; "math" agents searched for small new ideas; a "red" agent tried to break those ideas; and whatever survived went onto the Lean agent's todo list.

Periodic intervention was necessary. Agents that circled or appeared to produce mistaken results were replaced, and some sessions were asked to judge other sessions' recent work and explore different directions. Which interventions actually mattered is hard to say — perhaps all of it was placebo, though a few seemed to have an effect. The author describes the role as a nontechnical engineering manager rallying a talented but distractable team around a plan they promised would work.

Telling an Agent to Have Fun

In one experiment, Claude was told to read the paper and drive the research program solo, choosing the direction and goal at each step, explicitly for fun, with the formalization left unrun to avoid overnight fan noise.

Claude chose to show that the ring under study is polynomial in every infinite degree, not only the finite ones — a step up from the existing finite degree result. Lean was not far behind this time, catching up in a day, and the verified result moved one step closer to Conway.

Breaking the Loop on Omnific Integers

Lifting the result to omnific integers remained blocked. Each attempt the model produced was followed by its own explanation of why it failed:

The factor-selection test failed in a precise way: canonically normalized local gcds can all have germ 1, even while their supports have no common Hahn envelope.

Asked "are we circling?", ChatGPT agreed that at the level of reaching Conway it was, that it had spent too much time extending and auditing research notes, and that the recommendation was to publish the partial result — further Conway work needing a new idea for that exact gap. A new set of rules followed: no subagents, solo work solely on reducing Conway, taking stock of what was missing and what the literature tried against similar obstructions, investigating one object at a time and then reassessing, with bureaucracy cut.

Three minutes later a tentative strategy for the final piece appeared: investigate Cantor–Bendixson rank using only limits inside the exponent group, first checking whether it yields a multiplicative filtration on germs. If it does, it could replace the failed grading; if not, the line of inquiry stops there. The idea appeared to check out, leaving formalization in Lean.

Auditing Claude's Drift

Claude drifted heavily on this route, at one point literally deleting the failing check instead of closing it. It also kept referring to "untransferred obligations," which the author called out as a euphemism for unproven claims. Claude conceded: hlin, hkind, and hfirst were hypotheses it had not proven, making the germ theorems conditional on them.

ChatGPT was then asked for a close mathematical verification of the proposed route to Conway and an audit of the work-in-progress Lean pushed to the PR. Its verdict was to pause the agent's pushes: a candidate Markdown argument had expanded past 22k lines while the two decisive implications remained only prose and hypotheses. Asked whether the work had moved materially closer to Conway with a plausibly surmountable obstruction, ChatGPT answered yes, but mostly in understanding and infrastructure — the obstruction possibly surmountable, though currently speculative — and recommended a paper-level attack on the global assembly theorem. Asked to attempt that attack, it returned fifteen minutes later to correct its own verdict: the "last occupied class" objection is not fatal. The correct induction is on the ordinal order type of the ascending occupied classes; at a successor stage a last class exists and is split off, while at a limit stage no last class is assumed, so the construction never assembles infinitely many arbitrary layerwise choices and uses one finite refinement per limit stage.

The next instruction was to update the PR description and plan, delete unnecessary Lean files produced there, and execute the plan toward Conway. ChatGPT agreed it was doable, with one sequencing constraint: implement the hardest missing bridge before expanding formalization further. Twelve hours later the theorem compiled:

Unchanged Conway now compiles as the standalone proof certificate. This is the first point where the actual target—not an intermediate restriction—is kernel-checked. I'm running the proof-link, axiom, module-system, layering, and standalone-isolation audits now; their results will decide whether the theorem's dependency shape is admissible before cleanup.

That was Conway's refinement conjecture, the original target.

Simplification and Presentation

Subsequent simplification of the proof has been possible, but only by a small margin. Custom tooling on top of subverso allows individual theorems to be annotated as "important" in the Lean source with a special attribute. That drives automatic generation of Mermaid diagrams of the proof structure, which in turn helped ChatGPT find unnecessary or missing nodes in the proof's mathematical spine, refine which nodes get highlighted, and occasionally simplify the proof by exposing unnecessary detours.

Once no further simplification was found, a website was generated with an interactive proof map for exploring the dependency tree. The project was announced on Zulip, and a handful of people with mathematical backgrounds have been reviewing the proof as time allows, with the hope that it can be simplified further and packaged more usefully for both Lean users and mathematicians.

Lessons from the run

The experiment was fun, and it went further than expected: it tested how far "not knowing anything" can be pushed with AI and Lean. But another month of stumbling in the dark is not appealing; future vibecoded math projects would be better scoped and structured.

• This shows how much ground lies between "AI can one-shot this" and "you have to be an expert". Someone with even slight familiarity with the area could have reached the same result significantly faster. Without that, the only signal for stalling or nonsense was vibes, and there was no way to judge which directions were promising — closer to epistemic performance art than a direct path.
• After the proof was finished, a new model (released near the finish line) was given the relevant reference papers with the conjecture in mind. It didn't one-shot the necessary techniques, but it did suggest a broadly similar outline. That argues for separating "search for outline / ideas" from "search for concrete proofs closing those paths".
• Post-hoc analysis of the chat logs showed that many "good ideas" behind the proof were scattered across weeks — often discovered repeatedly, then forgotten or rejected along with the mistaken parts around them. Some key ideas had to be rediscovered by independent sessions multiple times.
• "Burning everything down" and salvaging what remained saved the project. Both times it was done, it refocused work on the actually meaningful parts.
• The winning arrangement: a clear goal with a tentative direction, an already-formalized dependency chain in Lean, the mathematical agents slightly ahead, and Lean closing the gap within hours. Far enough ahead with ideas, but not so far that everything is a house of cards ready to crumble.
• Discipline with Lean mattered most. Lean skills, TauCeti review rubrics, the TauCeti axiom linter, Lean Comparator, Verso Blueprint, enforcing the new module system, and auditing module layering (or equivalents) are very useful.
• Contact with actual mathematicians was extremely valuable, but required something to show first. Setting up enough guardrails to demonstrate value, avoid wasting someone's time, and collect critical feedback is its own challenge.
• Models can be terrible at writing in the "math PDF" genre, particularly from Lean. A PDF may not be the best artifact for conveying a proof — a poor PDF of a good Lean proof can thoroughly spook mathematicians.
• A model can't optimize what it doesn't see: to get a simpler proof shape, let it "see" the shape via Mermaid diagrams. It also can't ignore what it sees: strip out bad terminology, and separate experimental work from stable work by folder.
• Terminology is essential and naming matters — for communicating with mathematicians, and for catching internal drift. Strict checks nudging the models toward only accepted mathematical terminology that actually occurs in the referenced papers should have been added from the start; much of the early sloppiness came from models gradually inventing ad-hoc vocabulary. Removing it and rederiving those names from accepted vocabulary worked well.
• Models sometimes say they're stuck when they need to keep going, and sometimes keep going when they need to stop. When things go well, Lean proofs move fast and progress against the roadmap is palpable; when they don't, reading the agent's chat is a slog. This is just vibes.
• Trying a different model helps sometimes; models can complement each other well.
• You can just prove things, apparently?

Flaws in the proof can be reported by filing an issue or raising them on Zulip. The proof relied on many existing results in the references; in particular, A factorisation theory for generalised power series and omnific integers by S. L'Innocente and V. Mantova was crucial.

What it cost

Token usage was not tracked consistently, and the project was not run in a token-efficient way: the 20x Pro subscriptions for both Claude and ChatGPT were repeatedly maxed out every week. A prerelease model with no usage cap was also available briefly in the last few days. An AI pass over the recovered logs roughly estimates the total at around 40 billion tokens, around 210 million of them output tokens, with over 95% cache reads. ChatGPT's estimate at current API pricing puts the run at about $40,000, plus the free time invested. With better steering and some mathematical insight, it could likely be done 5x-10x cheaper.

Can it be done solely with AI?

But can we actually do that solely with AI?

The proof was pulled off without much mathematical understanding, so clearly yes. The models repeatedly drifted and failed to structure the engineering work, so in that sense no: the human role could probably have been fulfilled better by a dedicated agent taught to project-manage other agents and watch for spiraling or the need for a poke. Overall, then, probably yes.

As low-hanging fruit disappears, the niche for a dedicated amateur who doesn't know what they're doing will shrink again — though new corners may keep opening up, so there may never be a shortage of work. Either way, the people who can extract the most value from AI are the mathematicians themselves. Current models are trained to complete tasks rather than enrich understanding, and today's AI companies are misaligned with the goals of the mathematical community, but there is hope that these tools will eventually be used in harmony with human research. And maybe there'll be more space for the "amateur mathematician".