A Lean formalisation of the disproof of Ramaekers's conjecture
Abstract
We describe Redhill, a Lean formalisation of the major results in Hölzl, Kleine and Stephan's "Improved Lower Bounds for Strong n-Conjectures" (arXiv:2409.13439). Design decisions regarding types and data structures are justified as enabling canonical versions of the paper's claims, and from there the most direct proofs of said claims. The formalisation process also uncovered many errors, omissions and optimisation opportunities in the informal proof, all of which are addressed in the final library. Although Redhill is meant to stand alone, a few lemmas were upstreamed to the primary Lean mathematics library mathlib. We discuss the tension between upstreaming and leaving lemmas in separate libraries. Unlike many other contemporary formalisation projects, Redhill was completed without any assistance from large language models (LLMs). We compare our work with LLM-assisted projects, in particular an extension of arXiv:2409.13439 to n=4, aiming to establish design and style guidelines that define good Lean formalisations.
Related
- Remarks on the disproof of the unit distance conjecture
- On a classical zero-sum invariant II: Disproof of a long-standing conjecture
- Disproof of a conjecture of Ruscheweyh et al. on universal convexity of Ramanujan generating function
- Disproof of the dominating Hadwiger conjecture
- Infinitely Many Off-Critical-Line Zeros of the Tempered Xi Function: A Disproof of Yang's Conjecture
BibTeX
@misc{tan2026lean,
title = {{A Lean formalisation of the disproof of Ramaekers's conjecture}},
author = {Jeremy Tan},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.16323},
eprint = {2610.16323},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.16323},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A Lean formalisation of the disproof of Ramaekers's conjecture
AU - Jeremy Tan
PY - 2026
DA - 2026/10/12
PB - arXiv
DO - 10.48550/arxiv.2610.16323
UR - https://arxiv.org/abs/2610.16323
AB - We describe Redhill, a Lean formalisation of the major results in Hölzl, Kleine and Stephan's "Improved Lower Bounds for Strong n-Conjectures" (arXiv:2409.13439). Design decisions regarding types and data structures are justified as enabling canonical versions of the paper's claims, and from there the most direct proofs of said claims. The formalisation process also uncovered many errors, omissions and optimisation opportunities in the informal proof, all of which are addressed in the final library. Although Redhill is meant to stand alone, a few lemmas were upstreamed to the primary Lean mathematics library mathlib. We discuss the tension between upstreaming and leaving lemmas in separate libraries. Unlike many other contemporary formalisation projects, Redhill was completed without any assistance from large language models (LLMs). We compare our work with LLM-assisted projects, in particular an extension of arXiv:2409.13439 to n=4, aiming to establish design and style guidelines that define good Lean formalisations.
ER -