Vibing My Way to a Proof of Conway's Conjecture

By [Author], September 18, 2026 Price: Pay what you like

A few months back, the news cycle was dominated by AI's breakthroughs in mathematics. This sparked a question in my mind: could I—someone who is essentially a math noob—identify an unsolved mathematical mystery and use a frontier AI model to crack it?

After dedicating a full month of my spare time and burning through a massive amount of tokens, I believe I have successfully generated a Lean proof for a conjecture proposed by John Conway half a century ago.

The Core Claim: Conway's Refinement Conjecture

The conjecture posits that omnific integers possess a specific "refinement property." In formal terms:

$\text{If } ab = cd, \text{ then there exist integers } e, f, g, h \text{ such that:}$ $\begin{cases} a = ef \\ b = gh \\ c = eg \\ d = fh \end{cases}$

---

Current Status of the Proof

To be clear, this proof has not been independently peer-reviewed by professional mathematicians. However, I have several reasons to be optimistic:

• Mechanical Validation: It has successfully passed the automated checks of the Palomar registry.
• Expert Feedback: A handful of individuals proficient in both the Lean theorem prover and this specific mathematical niche have indicated that the statement appears correct.
• Kernel Integrity: Assuming there isn't a hidden bug in the Lean kernel, the proof is likely legitimate.

In the following sections, I will detail my methodology and the insights I gained.

---

The Philosophy of "Vibing"

Initially, I found the notion of "solving" a complex math problem without actually grasping the underlying theory to be utterly absurd. Naturally, that made the challenge even more enticing.

I didn't want a trivial result; I wanted a problem that felt magnetic.

Step 1: Selecting the Domain

I turned to Claude and asked it to suggest an open problem within the realm of surreal numbers.

What are Surreal Numbers?

For the uninitiated, surreal numbers are a system (invented or discovered?) by John Conway that encompasses every conceivable number—the infinitesimally small and the unimaginably large.

The beauty of this system—which I suspect appeals to the programmer's mind—is that it emerges from a single recursive rule: Create a new number in every available gap between existing numbers (including the gaps at the furthest ends).

The "Birth" Process:

1. Day 0: No numbers exist. The only gap is "nothing | nothing." $\rightarrow$ 0 is born.
2. Day 1: Two gaps appear: "nothing | 0" and "0 | nothing." $\rightarrow$ -1 and 1 are born.
3. Day 2: Four gaps appear (e.g., between -1 and 0). $\rightarrow$ -2, -1/2, 1/2, 2 are born.
4. Day 3: Eight gaps are filled. $\rightarrow$ -3, -3/2, -3/4, -1/4, 1/4, 3/4, 3/2, 3 are born.

If we continue this for an infinite number of days, we capture all real numbers and the first infinitesimals ($\omega, 1/\omega$). If we continue through transfinite iterations (infinities of infinities), we birth every ordinal and beyond.

Visual Note: As illustrated by Joel David Hamkins, this binary tree structure creates a consistent arithmetic for a truly vast number system.

Step 2: Pinpointing the Problem

I engaged Claude in a dialogue to narrow down a target:

Me: Which unsolved problems in the Surreal Numbers research program pull you the most and why?

Claude: [Suggested several options, noting recent progress in some].

Me: Get up to speed on the corners you want to know more about.

Me: What direction pulls you most?

Claude: Specifically, the question the L’Innocente–Mantova machinery just sharpened to a point — is every irreducible in $K((\mathbb{R}^{\le 0}))$ with infinite support prime? — which, by their reduction, is now exactly equivalent to Conway’s 1976 conjecture that any two factorizations of an omnific integer admit a common refinement.

Why this problem?

1. Legacy: It is purportedly the last of Conway's original conjectures regarding surreal numbers still unsolved.
2. Timing: 2026 marks the 50th anniversary of his seminal work, On Numbers and Games (ONAG).
3. Formalizability: I needed to ensure the problem could be stated concisely in Lean; otherwise, no mathematician would bother reviewing a "vibed" proof. Claude assured me this was possible.

The Roadmap

My process can be summarized as follows:

• Identify a field of interest (Surreal Numbers).
• Use AI to find a concrete, open conjecture.
• Verify the conjecture's historical significance (ONAG 50th).
• Formalize the statement in Lean.
• Iterate with the model to produce a proof.
• Obtain independent human verification.

---

Post-scriptum: I should note that Claude was slightly overconfident; it claimed the problem had been "perfectly reduced," but in reality, completing the proof required more nuance than the AI initially suggested.

-- Conceptual snippet of the conjecture statement
theorem conway_refinement_conjecture 
  (a b c d : OmnificInteger) 
  (h : a * b = c * d) : 
  ∃ (e f g h : OmnificInteger), 
    a = e * f ∧ b = g * h ∧ c = e * g ∧ d = f * h := 
begin
  sorry -- The "vibed" proof goes here
end