Erdős·erdos:1007
Erdős Problem 1007
Machine-checked by Palomar.
Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
graph theory·Source
AI activity
How grades workNew proof found (Lean)
Reasoning and sources
Autonomy
AI building on literature supplied to it
Details
literature: 🟢 House (2013); 🟢 Chaffee and Noble (2016)
Sources
House (2013)
Reasoning and sources
Autonomy
Secondary contribution: formalization
Details
proof to formalize: House (2013)
Sources
Does the formal statement say what was claimed?
F3 anchored The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Checks
2-
verified Palomar
Registered by Palomar at 43f89415: Comparator confirmed 1 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel
-
verified Palomar
Registered by Palomar at 85032a43: Comparator confirmed 1 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel
Declared by the projects
2Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.
Unit-distance graphs of dimension four with nine edges
- authors
- Dishant Shah
- method
- agent — claude-opus-5, claude-opus-5-5, glm-5.3-flash, gpt-6-astra, grok-4.7
- review
- agent-reviewed (gpt-6-astra (Codex CLI): adversarial review of the statement, claude-opus-5-5 (Claude Code): independent review of the proof, Dishant Shah: sign-off on the meaning of the statement-level declarations)
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 3 main results named, checked with Comparator, with an alignment table
- sources
- Dimension 4 and dimension 5 graphs with minimum edge set — formalizes, authors not-contacted; A 4-dimensional graph has at least 9 edges — background, authors not-contacted; On the dimension of a graph — background; Embedding graphs in Euclidean space — background
- related
- google-deepmind/formal-conjectures/blob/2a46c7bd74505b85f4967475bb733ded0ef8d348/FormalConjectures/ErdosProblems/1007.lean — builds-on; plby/lean-proofs — independent
- divergences
- None in meaning. The statement is formal-conjectures' erdos_1007.variants.dimension_four_extremal with its supporting definitions inlined and its ℝ^n notation written out as EuclideanSpace ℝ (Fin n). With both builds loaded together, the inlined statement is equal to the upstream declaration's type by rfl, and the proof elaborates against that type using only propext, Classical.choice and Quot.sound (docs/upstream-check-2026-09-22.md). Two earlier reviews checked the same equality against copies of the upstream definitions (docs/red-team-2026-09-20.md, docs/review-2026-09-22.md). The statement carries the upstream hypothesis that no vertex is isolated. It is necessary: adding isolated vertices to K_{3,3} changes neither the dimension nor the edge count, and a kernel-checked companion proves the statement false without it.
- checked by
- Palomar
Erdős 1007, dimension five: fifteen edges, attained by K6 and K1,3,3
- authors
- Dishant Shah
- method
- agent — Grok 4.7 500K Extra High Fast, claude-opus-5-5, glm-5.3-flash, grok-4.7-build
- review
- agent-reviewed (grok-4.7-build (Grok CLI): independent check of the statements against upstream, by rfl, claude-opus-5-5 (Claude Code): independent review of the proof, Dishant Shah: sign-off on the meaning of the statement-level declarations)
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 1 main results named, checked with Comparator, with an alignment table
- sources
- Dimension 4 and dimension 5 graphs with minimum edge set — formalizes, authors not-contacted
- related
- google-deepmind/formal-conjectures/blob/2a46c7bd74505b85f4967475bb733ded0ef8d348/FormalConjectures/ErdosProblems/1007.lean — builds-on
- divergences
- None in meaning. The statements are formal-conjectures' erdos_1007.variants.dimension_five and erdos_1007.variants.dimension_five_extremal, with their supporting definitions inlined (UnitDistanceEmbeddable, HasDimension and K133) and the ℝ^n notation written out as EuclideanSpace ℝ (Fin n). With both builds loaded together, each inlined statement equals the upstream declaration's type by rfl. A model of a different lineage from the one that wrote the statements ran that check (docs/upstream-check-stage1.md). Both proofs also elaborate against upstream's declaration types in one environment (docs/upstream-check-2026-09-23.md). The proof works with the library's copies of the two definitions, which have the same bodies, and rfl identifies them (docs/review-2026-09-23.md, check 2). Neither statement has a hypothesis, so there is none to drop. Kernel-checked separating examples show that each definition differs from its nearest plausible misreading, and satisfiability witnesses show that neither claim is vacuous.
- checked by
- Palomar
Follow and discuss
All discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal material
Formal statements · 1
Recorded elsewhere
Compare the registriesAlso known as · 3
- https://www.erdosproblems.com/1007
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1007.lean
- FormalConjectures/ErdosProblems/1007.lean