E571: “Does every rational exponent in [1,2) occur for one bipartite Turán graph?”

Prior art

September1,2026 announcement, Additional Attempts: full solution to Erdős571 by GPT-6 Astra.

Contributors

@declangessel

@woshuajolk

Verification

Verdict report: artifact 2fda9759

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

/-
Adapted 2026-09-05 for Jig330 from the proof by GPT-6 Astra in the Epoch AI
FrontierMath Erdős campaign (Tom Adamczewski and Thomas F. Bloom).
Public source: https://github.com/tadamcz/erdos571
Pinned commit: 661cc1d842c54661f55046d27abef531d0583b1e
Original module: Erdos571/Resolutions/Erdos571_325usd_42h.lean
Apache-2.0; accompanying LICENSE and NOTICE retained in campaign-discrete/erdos571-public.
Local changes: narrow Mathlib imports and port from Lean 4.28 to Jig's pinned Lean 4.33.
This is a port of existing mathematics, not a new solution discovered in this campaign.
-/
import Mathlib.Combinatorics.SimpleGraph.Bipartite
import Mathlib.Combinatorics.SimpleGraph.Copy
import Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.Asymptotics.Theta
import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

EpochPort.lean

Statement	User	Model	Harness	Time
2)V2The rational endpoint α=1 lies in the conjecture's interval [1,2).	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V3For every rational α with 1≤α<2, there is one finite bipartite graph G and positive constants c,C such that e…	@woshuajolk +1	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The rational endpoint α=1 lies in the conjecture's interval [1,2).

kernel-checked, filed Tue Aug 25 2026 08:41:52 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. forced-answer smoke for the exact rational interval convention.

1) V3 For every rational α with 1≤α<2, there is one finite bipartite graph G and positive constants c,C such that every sufficiently large n has c n^α≤ex(n;G)≤C n^α.

prior art, filed Tue Aug 25 2026 08:40:46 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @declangessel

Scope. Single finite bipartite forbidden graphs; ordinary subgraph containment; two-sided eventual real-power bounds.

E571:Erdős Problem #571 “Does every rational exponent in [1,2) occur for one bipartite Turán graph?”

E571: “Does every rational exponent in [1,2) occur for one bipartite Turán graph?”