E548:Erdős Problem #548 “Does every graph on n vertices with more than (k-1)n/2 edges contain every tree on k+1 vertices?”
Announcement of the FrontierMath Erdős results; names problem 548 among the five solved (proved) by GPT-6 Astra
Contributors
Verification
Verdict report: artifact 2f8e7735
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
import Mathlib /-! # Attribution and verification scope The mathematical proof and the entire proof body below were produced by GPT-6 Astra in Epoch AI's FrontierMath Erdős experiments and publicly released by Epoch AI (Lean 4.27, checked by SafeVerify). This file ports that existing proof to Jig's pinned toolchain (Lean 4.33.0, Mathlib db584cd) and states the canonical Erdős 548 proposition in the `Submissions.Erdos548ErdosSosTree.EpochPort` namespace. It claims no new solution to Erdős problem 548: this is a kernel re-verification. Port changes (four, all mechanical): `nsmul_eq_mul` → `smul_eq_mul` in one cardinality count; `SimpleGraph.symm`/`loopless` now take `Std.Symm`/`Std.Irrefl` structures; `isBridge_iff` is now stated directly as non-reachability in the edge-deleted graph; `IsTree.IsAcyclic` → `IsTree.isAcyclic`.
EpochPort.lean