VibeMathedMath problems solved with AI
Sign in

Erdős Problem #571: rational exponents for bipartite Turán numbers

Erdős problem #571 · erdosproblems.com/571

For every rational α∈[1,2)\alpha\in[1,2), there exists a finite bipartite graph GG such thatex⁡(n;G)=Θ(nα). \operatorname{ex}(n;G)=\Theta(n^\alpha). Equivalently, every rational exponent between 11 and 22 occurs as the order of growth of the Turán number of a single bipartite graph.

Result
Proved(see note)
Status
Resolved
AI contribution
AI-discovered
Method
Argument
Field
Graph theory
Posed by
Paul Erdős, Miklós Simonovits
Year posed
1974
Years open
52y
Solved
2026-08-26
Model
GPT-6 Astra (pre-release)
Vendor
OpenAI
Collaborators
Tom Adamczewski
Verification
Lean-verified
Publication
Announced
Significance
52 / 100
Disclosed cost
$617
Wikipedia
No dedicated article

What was actually shown

For every rational α\alpha satisfying1≤α<2, 1\le\alpha<2, the Lean theorem constructs some finite qq and a bipartite graphG:SimpleGraph⁡(Fin⁡q) G:\operatorname{SimpleGraph}(\operatorname{Fin} q) such thatex⁡(n;G)=Θ(nα) \operatorname{ex}(n;G)=\Theta(n^\alpha) as n→∞n\to\infty.

This resolves the single-graph rational-exponents conjecture. Earlier work of Bukh and Conlon proved the corresponding statement only for a finite family of forbidden bipartite graphs, and subsequent work realized many large classes of individual rational exponents. Astra's theorem covers every rational α∈[1,2)\alpha\in[1,2) with one forbidden graph for each exponent.

What the AI did

A pre-release GPT-6 Astra autonomously found the proof and wrote its Lean formalization in the FrontierMath Erdős benchmark, with no human seeing or steering the proof search. The roughly 10,000-line development constructs balanced rooted graph models for every rational exponent and proves closure operations that preserve the required extremal-number behavior, including edge subdivision by paths of arbitrary length, adding hubs to the two colour classes, and positive rooted powers. These constructions are combined to realize every rational α∈[1,2)\alpha\in[1,2) by a single finite bipartite graph.

Verification

Lean-verified. Checked here on 6 September 2026 from a clone of tadamcz/erdos571 at 661cc1d: 10,460 lines of Lean, zero sorry outside the statement stubs, zero axiom declarations, no native_decide, unsafe or implemented_by; Comparator configuration present and CI runs it with only propext, Quot.sound and Classical.choice. The statement was autoformalized for the benchmark and reviewed by Thomas Bloom; it uses mathlib's extremalNumber and IsBipartite and Asymptotics.IsTheta, and the repository's README compares it to the informal statement. One grep hit for the word 'externally' in a docstring is the only match for the risky-feature scan. erdosproblems.com, the field's own record, marks the problem PROVED (LEAN) with a proof exposition by Thomas Bloom, which is why this is Resolved rather than Candidate: the canonical tracker has accepted it.

Sources

Submitted by VibeGene on

Changelog2 changes

Discussion