{"id":"palomar/PALOMAR-2026-09-03-000002","url":"https://github.com/gaearon/conway-refinement/tree/63797aae79c09df5be6bfa066f147fa39e63b6cd","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-03-000002-v1.json","repo":"https://github.com/gaearon/conway-refinement","tags":["math.LO","math.RA","msc:13F25","msc:13F15","msc:13A05","msc:03E10","surreal-numbers","factorisation","lean-formalization"],"score":0,"title":"A proof of Conway's refinement conjecture","trust":"high","domain":"math.LO","source":"palomar","authors":["Dan Abramov"],"reviews":0,"subject":"math.LO","summary":"A Lean proof of Conway's 1976 refinement conjecture for omnific integers. For omnific integers a, b, c, d with ab = cd, it proves the existence of omnific integers e, f, g, h satisfying a = ef, b = gh, c = eg, and d = fh, including zero and degenerate cases. The proof proceeds through factorisation and refinement theory for generalised-power-series integer parts and connects the generalised-power-series and surreal-number formulations.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true}