Import the Erdős–Sós conjecture proof (Erdős Problem 548)

[Vilin97]

Summary

Imports the machine-checked proof of the Erdős–Sós conjecture (Erdős Problem 548, 1962): every graph on n ≥ k+1 vertices with at least (k−1)n/2 + 1 edges contains every tree on k+1 vertices as a subgraph. The conjecture had been open for six decades ("one of the most tantalizing problems in extremal graph theory" in Chung's collection; $100 Erdős prize). erdosproblems.com now lists it as PROVED (LEAN) with an exposition by Thomas Bloom, Formal Conjectures marks Erdos548.erdos_548 as research solved, and follow-up expositions have already appeared on arXiv (2609.15893, 2609.17877).

New project: LeanPool/Erdos548/ (3 modules, 1,313 lines) with card erdos548.

Upstream, announcement, license, provenance

• Upstream: https://github.com/tadamcz/erdos548 at commit c02708a6956d7b953c2e889c8bc24a0c97796313 (proof file Erdos548/Resolutions/Erdos548_192usd_21h.lean, unchanged since the initial packaging commit 8c2a3cf of 2026-09-03T21:56Z UTC).
• Announcement: repository published 2026-09-03 (the day GPT-6 Astra was released and Epoch AI reported its FrontierMath Erdős results); inside this run's eligible window [2026-07-18T09:45Z, 2026-09-11T09:45Z).
• License: Apache-2.0 (upstream LICENSE). The headline statement was produced by the FrontierMath Erdős autoformalization pipeline (epoch-research/LeanOpenProblems, MIT) and reviewed for faithfulness by Thomas Bloom; Google DeepMind's Formal Conjectures now carries the identical statement (Apache-2.0).
• Provenance: AI. The Lean proof was written autonomously by a pre-release GPT-6 Astra in the FrontierMath Erdős benchmark harness ($192, 21 h); Tom Adamczewski (Epoch AI) packaged it. No human wrote or steered the proof.
• Faithfulness: Erdos548.erdos_548 is verbatim the benchmark / Formal Conjectures statement. T.IsContained G is Mathlib's "injective graph homomorphism" (not-necessarily-induced subgraph), G.edgeSet.ncard the edge count, vertex types Fin n / Fin (k+1). The only divergence from the classical phrasing ("more than (t−2)n/2 edges") is half an edge in the odd-parity case; the internal lemma tree_free_edge_bound proves the sharp classical form 2|E| ≤ (t−2)n for every tree-free host.

What the proof is

Bloom's exposition: double counting over permutation words of the host vertices. For each word, distinguish the first letter as the root image and count cut positions ending at a neighbour of the root that support a rooted copy of the tree. Rotating the first qualifying prefix past the rest of a cut gives a gluing inequality for two branches at a common root (marked_word_gluing_count); reversing both blocks at a cut moves the root to a newly attached leaf, losing at most one word per permutation (rooted_word_leaf_move_count). Strong induction on the order t of the tree gives rooted_word_tree_bound (marked cut words ≤ rooted-copy count + (t−2)·n!); the marked count equals 2|E|·(n−1)!, so a tree-free host has 2|E| ≤ (t−2)n.

Reusable pieces: the word-combinatorial gluing/transfer inequalities (Words.lean, graph-free), attachLeaves with copy extension, RootedWordFamily/rootedWordCount, tree_edge_partition/tree_root_partition (splitting a tree at an edge or at a root, with cardinalities), leafRestoreIso.

Porting changes (Lean/Mathlib v4.28.0 → v4.34.0)

• SimpleGraph fields symm/loopless are now classes (constructor step); isBridge_iff no longer returns a conjunction; deprecated if_pos/if_neg/dif_pos/dif_neg, IsTree.IsAcyclic/isConnected, push_neg renamed; haveI → have in Prop goals; one Nat.cast_id needed in a simp only; unused [Fintype V] binder → [Finite V].
• Removed the upstream set_option maxHeartbeats 1000000 (every proof elaborates under the default; the heaviest is 0.2 s).
• Replaced import Mathlib by specific imports (found with #min_imports, layer by layer); split the 1,243-line file into Words (pure list/finset combinatorics), RootedTrees (graph part), Main (headline); docstrings on every definition; spacing and 100-column fixes. No statement was changed.

Trust / axiom audit

#print axioms for erdos_548, tree_free_edge_bound, rooted_word_tree_bound, marked_word_gluing_count: [propext, Classical.choice, Quot.sound]. No sorry/admit/native_decide/axiom/unsafe/partial/set_option/nolint/diagnostic commands (textual scan); the pool's option-backdoor environment audit over the four modules returns nothing.

Checks run locally

• lake build LeanPool.Erdos548: 0 errors, 0 warnings (with the lakefile's weak.linter.mathlibStandardSet).
• lake exe runLinter on all four modules: passed. lake exe lint-style LeanPool: exit 0. lake exe mk_all --check: no update necessary.
• python -m lean_pool.quality (run_checks, --skip-lean-axioms, generated card check): no findings for this project (the single-project worktree cannot #check other projects' declarations; CI does).

Compile-time measurements (quiet machine, 32 cores, Mathlib v4.34.0 oleans warm)

version	serial lake env lean	max RSS	clean lake build wall
upstream file verbatim, import Mathlib, heartbeat override (baseline)	4.8 s (import load alone 2.5 s)	7.3 GB	—
8-module split, narrowed imports	13.6 s (8 × ~1.4 s import load)	2.1 GB	7.5–8.3 s
final 3-module layout	5.7 s (Words 1.75, RootedTrees 2.08, Main 1.86; import load ≈ 1.4 s each)	2.1 GB	5.8 s

Elaboration proper dropped from ≈2.3 s to ≈1.4 s once the broad import was gone; the +0.9 s of serial CPU versus the baseline is the import load paid three times instead of once, traded for −71 % memory and a dependency closure of a dozen Mathlib modules instead of all of Mathlib. Hot spots (profiler, threshold 100 ms): erdos_548 0.21 s (nlinarith), rooted_word_tree_bound_aux 0.17 s, rootedWordFamily_glue 0.14 s; nothing else above 0.13 s.

Dedup

No Erdős–Sós/548 project in LeanPool/projects.yml, no prior PR. The only other public formalization (Jayyhk/erdos-lean, unlicensed) is a copy of the same Astra proof.

🤖 Generated with Claude Code

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

The PR appears safe to merge; no actionable issue remains at the current head.

Summary

This PR imports a complete machine-checked proof of the Erdős–Sós conjecture as a new independently registered Lean Pool project.

• Adds pure marked-word counting and permutation machinery.
• Adds rooted-tree copy, gluing, leaf-transfer, and tree-partition infrastructure.
• Proves the sharp tree-free edge bound and derives the registered Erdos548.erdos_548 theorem.
• Aligns the project umbrella, aggregate imports, and catalog metadata.

_{Reviews (4) · Last reviewed commit: "Merge branch 'main' into claude/daily-im..."}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 23.97 s (= 0.40 min) — user 16.14 s, sys 4.74 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 256 maxHeartbeats units across 4 files (1,333 added LOC).

Sum of lean --profile: 10278.6 ms (= 10.28 s). Import-excluded time: 6349.6 ms (= 6.35 s).

Count-heartbeats wall-clock total: 13.03 s. Repeated import cost inside lean --profile: 3929.0 ms (= 3.93 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/Erdos548/Words.lean	608	156	2.60	3.37	2.49	0.88	39	0
LeanPool/Erdos548/RootedTrees.lean	545	84	3.71	3.55	2.53	1.02	21	0
LeanPool/Erdos548/Main.lean	160	16	3.75	2.17	1.16	1.01	4	0
LeanPool/Erdos548.lean	20	0	2.97	1.19	0.17	1.02	0	0
Total	1,333	256	13.03	10.28	6.35	3.93	64	0

Aggregate phase totals

Phase	Time
import	3929.0 ms (= 3.93 s)
tactic execution	1732.0 ms (= 1.73 s)
interpretation	1569.0 ms (= 1.57 s)
typeclass inference	758.0 ms (= 0.76 s)
type checking	683.6 ms (= 0.68 s)
simp	395.5 ms (= 0.40 s)
elaboration	285.5 ms (= 0.29 s)
tacticAnalysis	271.8 ms (= 0.27 s)
linting	189.2 ms (= 0.19 s)
initialization	143.3 ms (= 0.14 s)
parsing	102.5 ms (= 0.10 s)
process pre-definitions	56.2 ms (= 0.06 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.Erdos548.Words	6.90 s
LeanPool.Erdos548.RootedTrees	3.40 s
LeanPool.Erdos548	1.20 s
LeanPool.Erdos548.Main	1.00 s

Per-file `lean --profile` output

LeanPool/Erdos548.lean

import took 1.02s
cumulative profiling times:
	elaboration 0.167ms
	import 1.02s
	initialization 34.1ms
	interpretation 131ms
	linting 0.303ms
	module linting 0.00128ms
	overlappingInstancesLinter 0.306ms
	parsing 0.0281ms
	tacticAnalysis 2.35ms
real 1.79
user 1.00
sys 0.81

LeanPool/Erdos548/Main.lean

import took 1.01s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 107ms
cumulative profiling times:
	attribute application 0.0416ms
	congr simp thm 3.2ms
	elaboration 20.3ms
	fix level params 0.725ms
	import 1.01s
	initialization 41.7ms
	instantiate metavars 1.67ms
	interpretation 403ms
	let-to-have transformation 0.0549ms
	linting 16.6ms
	module linting 0.00195ms
	norm_num 19.6ms
	overlappingInstancesLinter 4.32ms
	parsing 7.96ms
	process pre-definitions 4.84ms
	ring 13.1ms
	share common exprs 4.23ms
	simp 126ms
	tactic execution 171ms
	tacticAnalysis 27.4ms
	type checking 79.6ms
	typeclass inference 219ms
real 2.20
user 1.94
sys 0.80

LeanPool/Erdos548/RootedTrees.lean

import took 1.02s
cumulative profiling times:
	attribute application 3.77ms
	compilation (IR) 0.0278ms
	compilation (LCNF base) 0.265ms
	compilation (LCNF impure) 0.144ms
	compilation (LCNF mono) 0.131ms
	congr simp thm 11.4ms
	elaboration 131ms
	fix level params 4.01ms
	import 1.02s
	initialization 38.1ms
	instantiate metavars 9.5ms
	interpretation 535ms
	let-to-have transformation 3.29ms
	linting 77.2ms
	module linting 0.00178ms
	overlappingInstancesLinter 17.8ms
	parsing 45ms
	process pre-definitions 27.7ms
	share common exprs 12.5ms
	simp 171ms
	tactic execution 770ms
	tacticAnalysis 128ms
	type checking 263ms
	typeclass inference 281ms
real 2.53
user 3.23
sys 0.83

LeanPool/Erdos548/Words.lean

import took 879ms
cumulative profiling times:
	attribute application 0.584ms
	compilation (IR) 0.101ms
	compilation (LCNF base) 1.18ms
	compilation (LCNF impure) 0.511ms
	compilation (LCNF mono) 0.908ms
	congr simp thm 7.67ms
	dsimp 0.814ms
	elaboration 134ms
	fix level params 5.97ms
	import 879ms
	initialization 29.4ms
	instantiate metavars 7.8ms
	interpretation 500ms
	let-to-have transformation 0.389ms
	linting 95.1ms
	module linting 0.00133ms
	overlappingInstancesLinter 13.1ms
	parsing 49.5ms
	process pre-definitions 23.7ms
	share common exprs 13.9ms
	simp 98.5ms
	tactic execution 791ms
	tacticAnalysis 114ms
	type checking 341ms
	typeclass inference 258ms
real 2.32
user 3.21
sys 0.76

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[Vilin97]

Independent review (agentic, per .github/REVIEW_RULES.md) — verdict: approve

The GPT review workflow is disabled, so this is the independent review of record for this PR, run against the upstream source (tadamcz/erdos548 @ c02708a6), the diff, the build/profile evidence and CI on head d8000493.

Faithfulness — pass

• Erdos548.erdos_548 is character-for-character the benchmark statement (LeanOpenProblems apn/data/erdos_autoformalized/Isolated/Erdos548.erdos_548.lean @ 77882c43) and the Formal Conjectures statement FormalConjectures/ErdosProblems/548.lean; checked the type with #check: ∀ n k, k + 1 ≤ n → ∀ G : SimpleGraph (Fin n), (↑k - 1) / 2 * ↑n + 1 ≤ ↑G.edgeSet.ncard → ∀ T : SimpleGraph (Fin (k + 1)), T.IsTree → T.IsContained G.
• IsContained is Mathlib's Nonempty (T.Copy G) (injective homomorphism), so "contains as a subgraph, not necessarily induced" is what is proved; edgeSet.ncard over Fin n is the plain edge count; the rational inequality is (k−1)n/2 + 1 ≤ |E|. The card's headline informal says exactly this.
• No postulated content: the four card declarations depend on [propext, Classical.choice, Quot.sound] only; no structure field or hypothesis carries the hard step. tree_free_edge_bound (2·|E| ≤ (t−2)·n for every tree-free host) is the sharp classical form and is proved, not assumed.
• Read all 64 declarations. The argument is Bloom's permutation-word double counting: marked_word_gluing_count (rotation injection D → E), full_word_transfer_count (cut-reversal involution, at most one first cut lost per word), rooted_word_leaf_move_count, rooted_word_branch_gluing_count, tree splitting (tree_edge_partition via isBridge_iff, tree_root_partition with the cardinality bookkeeping |A| + |Aᶜ ∪ {r}| = t + 1), base case t = 2, strong induction rooted_word_tree_bound_aux, and full_word_base_count = (n−1)!·2|E|. The two card informals that omitted hypotheses (nonempty host word; common word length) were corrected in d8000493 after Greptile's P1.

Novelty — pass

No Erdős–Sós or #548 project in projects.yml, no prior PR, and no overlapping infrastructure in the pool (the only SimpleGraph.Copy users are CompactnessAndDegeneracy; no other project has tree-splitting or permutation-word counting). The other public formalization (Jayyhk/erdos-lean) is an unlicensed copy of this same proof.

Significance — pass

A 1962 conjecture central to extremal graph theory, resolved in full; erdosproblems.com marks it PROVED (LEAN) and three expository preprints appeared within two weeks (arXiv 2609.05417, 2609.15893, 2609.17877). It implies erdosproblems #547 and #557. The proof is 1.3k lines and elaborates in ~1.4 s, so the cost/value ratio is exceptional. Reusable pieces: graph-free gluing/transfer inequalities on permutation words, attachLeaves + copy extension, rooted-copy counting, tree edge/root splitting with cardinalities, leafRestoreIso.

Sources — pass

Upstream Apache-2.0 with a NOTICE (Apache §4(d) attribution to be reproduced in NOTICE.extra.yml by a follow-up non-content PR, as was done for the Köthe import in #409). Statement source LeanOpenProblems is MIT; the same text is Apache-2.0 in Formal Conjectures. Card source gives repo, commit and the benchmark paper title; provenance: AI is accurate (autonomous GPT-6 Astra, no human steering).

Code quality (advisory) — acceptable

• Port is mechanical (v4.28 → v4.34 API renames, Std.Symm fields, isBridge_iff shape); no statement changed. Heartbeat override removed (heaviest proof 0.21 s). import Mathlib replaced by twelve specific modules; RSS 7.3 GB → 2.1 GB per process.
• Style: warning-free under weak.linter.mathlibStandardSet, runLinter and lint-style clean, docstrings on every def, longest proof body 64 code lines (cap 200). Two attribute [local instance] Classical.propDecidable sections are inherited from upstream and scoped; they could be replaced by open scoped Classical in but do not affect trust.
• Compile cost (CI profile comment): 24 s lake build for the changed cone, 256 heartbeat units, import-excluded profile 6.4 s across four files. Three modules rather than eight were chosen because each graph module pays ~1.4 s of import loading; total serial CPU 5.7 s vs 4.8 s for the broad-import original, with a dependency closure of a dozen Mathlib modules instead of all of Mathlib.

CI on head d8000493

Build project ✅, Content / non-content separation ✅, Documentation preflight ✅, Greptile ✅ (P1 fixed, P2 answered: the 40-line guideline is the Python function rule; the Lean rule is the 200-line cap), Partial Port Audit ✅, Proof Profile ✅. The earlier "Build project" failure on 054ddd36 was the cancellation caused by the sync bot merging main (#451) into the branch, not a build error.

Findings

None blocking. Follow-up (non-content): add the upstream NOTICE text to NOTICE.extra.yml and regenerate NOTICE.