FrontierMath Ramsey Hypergraphs in Lean

Formalizing progress on Epoch AI's FrontierMath open problem on hypergraphs.

This repository formalizes lower bounds for the extremal hypergraph function introduced by Will Brian and Paul B. Larson in Choosing between incompatible ideals. The sequence arises as the finitary core of a Ramsey-theoretic problem about incompatible ideals and the simultaneous convergence of infinite series.

A hypergraph is said to contain a partition of size if there are and with such that every member of belongs to exactly one edge of . The extremal function is the largest for which there is a hypergraph with vertices, no isolated vertices, and no partition of size greater than .

The FrontierMath page presents warm-up, single-challenge, and full-problem variants. This repository addresses the full-problem variant: it formalizes an explicit construction showing

where Brian–Larson's recursive benchmark is given by

Thus the constant-factor improvement is already in effect at , exactly as requested in the FrontierMath full problem.

Asymptotic consequence. The repository also formalizes GPT-5.4 Pro's Lubell-family lower bound, which implies

Combined with Brian–Larson's upper bound (not formalized here)

this yields the sharp asymptotic formula

Note: on the finite side, the formalized construction gives . So this development resolves the FrontierMath full-problem prompt, while stopping one vertex short of the single-challenge target .

This Lean development is based on an informal proof produced by GPT-5.4 Pro. The prompters of that informal proof were Kevin Barreto and Liam Price; the original paper output is archived on Google Drive here.

Highlights

• The substitution theorem underlying the recursive witness constructions is formalized in Lean.

• Explicit uniform lower bound

• Lubell-frame asymptotic lower bound

• Asymptotic consequence

• The repository includes the full paper, blueprint, and the explicit Python constructor required by the FrontierMath problem statement.
• The current formal development is about 6,300 lines of Lean.

Repository structure

The core development is organized as follows:

• FrontierMathHypergraphs/Basic.lean — hypergraph definitions, partitions, the extremal function H, and the benchmark sequence k.
• FrontierMathHypergraphs/Substitution.lean — support patterns, frames, substitution hypergraphs, and the substitution theorem.
• FrontierMathHypergraphs/Uniform.lean — the finite bootstrap and the uniform lower bound.
• FrontierMathHypergraphs/Lubell.lean — Lubell frames and the asymptotic theory.
• blueprint/src/content.tex — blueprint source.
• frontier.tex and paper/input.tex — paper source.

Key links

• FrontierMath open problem: A Ramsey-style Problem on Hypergraphs
• Brian–Larson paper on ScienceDirect
• Original GPT-5.4 Pro paper output (Google Drive)
• Accompanying paper source in this repository
• Blueprint source in this repository

Useful commands

Compile the Lean files (requires Lean):

lake exe cache get && lake build

Build the blueprint PDF (requires uv):

uvx leanblueprint pdf

Build and serve the blueprint website:

uvx leanblueprint web && uvx leanblueprint serve

References

• Will Brian and Paul B. Larson, Choosing between incompatible ideals, European Journal of Combinatorics 96 (2021), Article 103349. DOI: 10.1016/j.ejc.2021.103349, ScienceDirect: link, arXiv: 1908.10914
• Epoch AI, A Ramsey-style Problem on Hypergraphs. FrontierMath open problem page: link
• GPT-5.4 Pro, A constant-factor lower bound for . Informal paper output archived on Google Drive; prompters: Kevin Barreto and Liam Price. Archive: link