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 $H(n)$ 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 $(V,\mathcal H)$ is said to contain a partition of size $n$ if there are $D \subseteq V$ and $\mathcal P \subseteq \mathcal H$ with $|D| = n$ such that every member of $D$ belongs to exactly one edge of $\mathcal P$. The extremal function $H(n)$ is the largest $k$ for which there is a hypergraph with $k$ vertices, no isolated vertices, and no partition of size greater than $n$.

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

$$ H(n) \ge \frac{26}{25},k_n \qquad (n \ge 15), $$

where Brian–Larson's recursive benchmark is given by

$$ k_1 = 1, \qquad k_n = \lfloor n/2 \rfloor + k_{\lfloor n/2 \rfloor} + k_{\lfloor (n+1)/2 \rfloor}. $$

Thus the constant-factor improvement is already in effect at $n=15$, 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

$$ \liminf_{n\to\infty} \frac{H(n)}{k_n} \ge 2\ln 2. $$

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

$$ H(n) < n\ln n + \gamma n + \tfrac12, $$

this yields the sharp asymptotic formula

$$ \lim_{n\to\infty} \frac{H(n)}{n\ln n} = 1. $$

Note: on the finite side, the formalized construction gives $H(20) \ge 65$. So this development resolves the FrontierMath full-problem prompt, while stopping one vertex short of the single-challenge target $H(20) \ge 66$.

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

$$ H(n) \ge \frac{26}{25},k_n \qquad (n \ge 15). $$

• Lubell-frame asymptotic lower bound

$$ H(n) \ge \frac{h_t-1}{\log_2 t}n\log_2 n - O_t(n) \qquad \left(t \ge 2 \text{ fixed},\qquad h_t:=\sum_{n=1}^{t}\frac{1}{n}\right). $$

• Asymptotic consequence

$$ \liminf_{n\to\infty} \frac{H(n)}{k_n} \ge 2\ln 2, \qquad k_n = \frac12 n\log_2 n + O(n). $$

• 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 $26/25$ 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 $H(n)$. Informal paper output archived on Google Drive; prompters: Kevin Barreto and Liam Price. Archive: link