---

Claim. The answer to Problem 1007 is $9$: every graph of dimension $4$ has at least nine edges, and $K_{3,3}$ is, up to isolated vertices, the only graph of dimension $4$ with exactly nine edges ($K_{3,3}$ with an isolated vertex added has the same dimension and edge count, so the uniqueness is read among graphs without isolated vertices, as the result page records). The claimed result is the main result of R. F. House, A 4-dimensional graph has at least 9 edges, Discrete Math. 313 (2013), no. 18, 1783--1789, a Note; the result is unnumbered, announced on p. 1783 after the paper's Definition 1 and Problem 2 and concluded on p. 1789, and the corpus states it on its result page main result. Definition 1 is the site's convention: an embedding places the vertices at distinct points of $\mathbb R^n$ with adjacent vertices at distance exactly $1$ and says nothing about non-adjacent pairs. The proof reduces the question to 43 biconnected candidate graphs of orders $6$ and $7$, counted from Read and Wilson's Atlas of Graphs, and embeds 42 of them in the plane or in $\mathbb R^3$ by drawings (Figs. 7, 10 and 11); the one left is $K_{3,3}$, whose dimension is $4$ by the value $\dim K_{m,n}=4$ for $m,n\ge3$ of Erdős, Harary and Tutte. The later paper of Chaffee and Noble (their claim page) reports this as the first proof of both statements.

Acceptance. Refereed publication in Discrete Mathematics (received 12 November 2012, accepted 9 May 2013, available online 4 June 2013, the date of this page, per p. 1783; the Crossref record dates the print issue September 2013). The site's curator, Thomas Bloom, labels the problem solved and credits the value and the uniqueness to House [Ho13] (the reviewed evidence; Bloom took no part in the paper); the proof-claim tab is empty. Read depth: this page rests on the statement on pp. 1783 and 1789 and on the proof's route; neither the drawings nor the Atlas count are checked, and nothing is independently reviewed by this project. The acceptance rests on the publication and the curator's credit.

Formalization. The file src/v4.29.1/ErdosProblems/Erdos1007.lean of Boris Alexeev's repository plby/lean-proofs (Lean v4.29.1 with Mathlib v4.29.1, import Mathlib its only import; 1,101 lines at the pinned commit of 2026-09-15, linked above), announced in the site's forum on 19 January 2026, declares itself a formalization of this result: its header names House, Chaffee and Noble as informal authors and the automated theorem-proving system Aristotle and Alexeev as formal authors. It defines a unit-distance embedding as an injective map into $\mathbb R^d$ with adjacent vertices at distance $1$, the site's and the paper's convention, sets GraphDimension G to the least such $d$, and proves erdos_1007 : IsLeast {n | ∃ V ... (G : SimpleGraph V), GraphDimension G = 4 ∧ G.edgeFinset.card = n} 9 through dim_K33_eq_4, K33_edges_final and edges_lt_9_embeds_in_3 (every graph with fewer than nine edges embeds in $\mathbb R^3$); a closing comment reports the axioms propext, Classical.choice and Quot.sound, and the file has no sorry, axiom, native_decide or unsafe. The forum post says that Aristotle was first given a proof that $K_{3,3}$ does not embed in $\mathbb R^3$ and organized the rest itself, and, in an update, that a second run proved the non-embeddability from the statement alone; it links the v4.24.0 copy, and the repository's note (the record link) lists copies for five toolchains. The formal-conjectures statement of the problem names this file in its formal_proof attribute under its own HasDimension, with no bridge between the two definitions in either file. Nothing was built, replayed or audited by this project and no outside examination of the file is published, so the page lists no formalized evidence; the acceptance rests on the refereed publication and the curator's credit. The same file is linked from the page of Chaffee and Noble, whom it also names. A second Lean development, Dishah3241/Erdos1007 (2026-09-23), proves the uniqueness half alone, following Theorem 7 of Chaffee and Noble; its README says that House's paper was not consulted, so it is linked from their page and not from this one.