AI Multi-Agent Workflow Produces Lean-Verified Proof of Conway’s Refinement Conjecture

The conjecture concerns the properties of omnific integers—the integer part of surreal numbers. It claims that these integers possess a refinement property: for any equality ab = cd, there exist integers $e, f, g, h$ such that a = ef, b = gh, c = eg, d = fh.

The researcher's methodology relied on a sophisticated setup of AI agents with specialized roles, such as "PM" agents for coordination, "Red" agents for adversarial review, and "Lean" agents for formal verification. By using tools like Codex and managing different model personalities—specifically the more "skeptical" nature of ChatGPT compared to the "grandiose" outputs sometimes seen in Claude—the researcher was able to filter through significant amounts of "hallucinated" or non-mathematical content.

The workflow required the formalization of existing peer-reviewed research into the Lean theorem prover to create a "grounded" foundation, preventing the agents from drifting into unsupported claims. While the researcher noted that the models struggled with the engineering and structural aspects of the project—often requiring human intervention to prevent "process theater"—the final result was a standalone, kernel-checked proof of the conjecture.