Rational Turán exponents of a single $k$-uniform hypergraph
Chang Liu, Jue Dai
math.CO
Nov 5, 2026 · v1
TL;DR
The main theorem on rational Turán exponents for single k-uniform hypergraphs is formalized in Lean 4 (AI-assisted), conditional on two stated axioms.
Abstract
For a fixed $k$-uniform hypergraph $F$, let $\mathrm{ex}_k(n,F)$ denote the maximum number of edges in an $F$-free $k$-uniform hypergraph on $n$ vertices. We prove that for every integer $k\ge2$ and every rational $r\in[0,1]$ there exists a $k$-uniform hypergraph $F_{k,r}$ such that \begin{equation*} \mathrm{ex}_k(n,F_{k,r})=Θ(n^{k-r}). \end{equation*} The case $k=2$ is the rational exponents conjecture of Erdős and Simonovits \cite{Erdos1988}, also known as Erdős problem #571 \cite{BloomErdoswebsite}; a proof was announced in September 2026 and is expounded by Conlon et al.\ \cite{Conlon-Janzer-Jiang-Kim-Lee-Liu-Longbrake-Yepremyan}. For $k\ge3$ the theorem extends their result to $k$-uniform hypergraphs. In the single-hypergraph setting, this strengthens Fitch's finite-family theorem \cite{Fitch} by realizing each exponent with a single forbidden $k$-uniform hypergraph for $0\le r\le1$. We also show, via an explicit two-edge construction, that for $k\ge4$ this strengthening fails for $\lceil k/2\rceil<r\le k-1$: no single $k$-uniform hypergraph $F$ then satisfies $\mathrm{ex}_k(n,F)=Θ(n^{k-r})$. The main result of this paper has been formalized in Lean 4, conditional on two explicitly stated axioms.
Problem
Extend the Erdős–Simonovits rational exponents conjecture (Erdős problem #571) from graphs to k-uniform hypergraphs, realizing each exponent k−r with a single forbidden hypergraph instead of a finite family.
Approach
The k-graph is built by suspending a balanced rooted bipartite graph from the graph case: a fixed (k−2)-set is added to every edge, and the result is raised to rooted powers. A suspension inequality transfers the graph upper bound, and a random algebraic argument gives the lower bound. A two-edge construction yields the obstruction result. Theorem 1.2 was formalized in Lean 4 with help from an AI system. The formalization assumes two axioms: the literature inputs and the uniform dichotomy.
Results
For every k≥2 and rational r∈[0,1] there is a single k-graph F with ex_k(n,F)=Θ(n^{k−r}). For k≥4 and ⌈k/2⌉<r≤k−1, no single F achieves this order. The Lean formalization covers Theorem 1.2 but not the obstruction proposition.
