Lean proof system verifies complex math conjecture disproof
A Lean formalisation of the disproof of Ramaekers's conjecture
Logic in Computer Science
Summary
The paper presents Redhill, a computer-checked formal proof that confirms and corrects a complex mathematical disproof from a previous paper. The authors carefully translated the original arguments into a precise computer language called Lean, which helped find and fix errors and missing parts. This makes the claims in the original math paper more reliable and easier to verify automatically. The authors also discuss differences between their manual approach and projects assisted by AI tools.
What this means in practice
- •For formal methods engineers: Use a mechanically verified Lean library to improve confidence in complex mathematical proofs and correct informal errors.
- •For mathematics software developers: Integrate verified lemmas from the Redhill formalisation into broader math libraries to enhance automated reasoning tools.
Authors
Jeremy Tan
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.