Erdős Problem #571: rational exponents for bipartite Turán numbers
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
For every rational $\alpha\in[1,2)$, there exists a finite bipartite graph $G$ such that
$$
\operatorname{ex}(n;G)=\Theta(n^\alpha).
$$
Equivalently, every rational exponent between $1$ and $2$ occurs as the order of growth of the Turán number of a single bipartite graph.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra (pre-release)
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 $\alpha\in[1,2)$ by a single finite bipartite graph.
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.
For every rational $\alpha$ satisfying
$$
1\le\alpha<2,
$$
the Lean theorem constructs some finite $q$ and a bipartite graph
$$
G:\operatorname{SimpleGraph}(\operatorname{Fin} q)
$$
such that
$$
\operatorname{ex}(n;G)=\Theta(n^\alpha)
$$
as $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 $\alpha\in[1,2)$ with one forbidden graph for each exponent.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.