I vibed a proof of Conway's conjecture

An AI-assisted project reports a formal proof of Conway's refinement conjecture, concerning an extension of the integers that includes infinite quantities. The conjecture asks whether two equal products can always be broken into common factors and recombined. The author's account describes a month of generating ideas, challenging them and translating surviving arguments into Lean, a system for checking formal proofs.

The repository separates the mathematical statement from its proof and reports checks against unapproved assumptions. That separation matters: a machine can check a proof of a precisely written statement, while mathematical review must also establish that the statement captures the intended conjecture. The README itself says the formal statement may not correspond to Conway's conjecture in some respect, and at publication the author said the proof had not been independently verified by mathematicians.