---

Claim. The answer to Problem 1010 is yes, for every $n$: if $t<\lfloor n/2\rfloor$, every graph on $n$ vertices with exactly $\lfloor n^2/4\rfloor+t$ edges has at least $t\lfloor n/2\rfloor$ triangles. The claim is a Lean development, the file src/latest/ErdosProblems/Erdos1010.lean of Boris Alexeev's repository plby/lean-proofs (first committed 26 August 2026), whose final theorem erdos_1010 (line 612 at the pinned commit of 2026-09-15, linked above) states: for every finite vertex type $V$ with decidable equality and every simple graph $G$ on $V$ with decidable adjacency, if $t<|V|/2$ (natural division) and G.edgeFinset.card = |V|^2/4 + t, then $t\cdot(|V|/2)\le$ the number of $3$-cliques of $G$. With $V$ the type of $n$ elements this is the statement of the problem for every $n$, with no largeness assumption. The claimant is Alexeev, whose repository publishes the file; the file names no author, human or machine, and the repository's note (the record link) describes it only as a formalized proof of the problem, so no system is named on this page.

The development. The main file (632 lines, headed leanprover/lean4:v4.33.0 mathlib v4.33.0) imports Mathlib modules and two of the $22$ files under ErdosProblems/Erdos1010/ in the same sources, which import the others. Its module docstring says that the proof uses finite maximum-cut charge bounds for even orders and a leaf-switching-and-deletion reduction for odd orders, that an earlier Goodman-based lower-bound inference was found invalid and is not used, and that the detailed proof is in the repository's tex/1010.tex, which this page does not describe. The argument is the file's own: it names neither Lovász and Simonovits nor Nikiforov and Khadzhiivanov, so it is recorded as an independent proof and not as a formalization of either published result. The main file and the $22$ submodules contain no sorry, no axiom and no native_decide; the files print no #print axioms output. The formal-conjectures statement erdos_1010 (added 20 September 2026, described on the problem page) names line 612 of this file in its formal_proof attribute; its statement is the theorem instantiated at Fin n.

Depends on. No page of this wiki; the development is self-contained over Mathlib.

Standing. Claimed. The development has not been built, audited or kernel-checked in this corpus, and no outside examination of it is published, so the page lists no formalized evidence. The site's label PROVED and the community database's record rest on the published proofs of Lovász and Simonovits and Nikiforov and Khadzhiivanov, and the problem's standing does not rest on this page. If built and audited, the theorem would settle the problem for small $n$ as well, where the 1983 chapter's statement carries a large-$n$ convention (the problem page's third remaining gap).