A Lean formalisation of the disproof of Ramaekers's conjecture
Jeremy Tan
math.NT
Oct 12, 2026 · v1
cs.LO
TL;DR
Presents Redhill, a human-written Lean/mathlib formalisation of lower bounds on strong n-conjectures disproving Ramaekers's conjecture, with lemmas upstreamed to mathlib.
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.
Problem
Hölzl, Kleine and Stephan gave lower bounds for strong n-conjectures that disprove Ramaekers's conjecture. The informal proof had not been machine-checked, and LLM-generated Lean repositories raise questions about what makes a good formalisation.
Approach
The author built Redhill, a Lean library that formalises the paper's major results. It uses canonical types such as Fin n → ℤ for tuples and ENNReal-valued tuple quality, together with prime chains and polynomial constructions for the disproofs. Several general lemmas on radicals, coprimality and integer products were upstreamed to mathlib via merged PRs. An LLM-written claimed disproof for n=4 was integrated into Redhill by hand, and its style was compared with LLM-assisted projects.
Results
The formalisation proves the disproof of Ramaekers's conjecture for all n ≥ 4, including a quality bound of at least 9/8 for n=4. It also uncovered errors, omissions and optimisation opportunities in the informal proof, all addressed in the library. The paper proposes design and style guidelines for readable Lean formalisations.
