---

Claim. Every graph with $n$ vertices and more than $n^2/4$ edges has an edge lying in at least $n/6$ triangles, the statement of Problem 905. The claimed result is N. G. Khadzhiivanov and V. Nikiforov, Solution of a problem of P. Erdős about the maximum number of triangles with a common edge in a graph, C. R. Acad. Bulgare Sci. 32 (1979), no. 10, 1315--1318, in Russian. The coauthor is V. (Vladimir) Nikiforov, as the 1988 paper's reference [2] and p. 44, Fox and Loh's reference [13] and Bollobás and Nikiforov's 2005 reference [10] give him; the site's reference text prints "S. V. Nikiforov". The note is not held and has no online record found; its statement is known through the 1988 paper of the first author (card). That paper states the problem in the site's exact form, with $\hat t$ the largest number of triangles on one edge (p. 44): if $e>n^2/4$ then $\hat t\ge n/6$; it says the author solved the problem completely with Nikiforov in the 1979 note; and it proves the statement again with a surplus as its Corollary 3 (p. 45): if $e>\lfloor n^2/4\rfloor$ then $\hat t>n/6$, from the inequality $(3t+\bar t)\hat t\ge nt$ of its Theorem 1 (which the paper says the 1979 note proves a little differently) and the bound $\sum_vd(v)^2>ne$ of its Lemma 4. Corollary 5 gives $\lceil n/6\rceil$ as the exact minimum of $\hat t$ for $n\ge4$ over the wider class of graphs with at least $\lfloor n^2/4\rfloor$ edges and a triangle; its figure 8 graph (p. 46, not checked) attains $\lceil n/6\rceil$ with $\lfloor n^2/4\rfloor+1$ edges only for suitable $n$ (never when $6\mid n$, nor for $n=4,5,6$), so the constant $1/6$ cannot be raised. The page name carries the year and the issue's nominal month: the note is number 10 of a twelve-issue volume, and no source read gives its day.

Depends on. Nothing in this wiki; the 1988 argument is self-contained, and the 1979 note is cited through it.

Acceptance. The reviewed evidence is documented acceptance by named experts and by the site's curator (T. F. Bloom), who is independent of the authors. Fox and Loh, in a refereed paper (Combinatorica 32 (2012); p. 2 of the preprint, recorded on the card for Problem 80), state that Edwards and Khadzhiivanov and Nikiforov proved that every $n$-vertex graph with more than $n^2/4$ edges has an edge in at least $n/6$ triangles. Khadzhiivanov's 1988 paper, in a university annual whose refereeing practice is not established, reproves the statement with the surplus above. The site's commentary credits the proof to this note and labels the problem proved, and the community database agrees. Bollobás and Nikiforov's refereed paper of 2005 (its own claim page, Bollobás and Nikiforov) credits the first proofs to Edwards and to this note and proves the statement again by another route; its second author shares the 1979 coauthor's name, so it is not counted as independent acceptance of this note. Whether the Comptes rendus of the Bulgarian Academy refereed the note is not documented, so refereed is not listed. Read depth: the 1979 text is not held; the 1988 statements are checked clause by clause and the proofs of Theorem 1 and Lemma 4 only for structure. Erdős's own 1982 and 1993 reports of the problem credit Edwards (see the problem page), not this note.

Formalization. The file src/v4.29.1/ErdosProblems/Erdos905.lean of Alexeev's repository plby/lean-proofs, linked above at the commit of 15 September 2026, declares itself a Lean formalization of this note's result, naming Khadzhiivanov and Nikiforov as its informal authors and, as formal authors, the AI systems Aristotle and GPT 5.4 and its human author, who announced it in the site's thread on 7 April 2026 (the account andresg535) with a link to type-check it online (the live.lean-lang.org link above, dated 7 April 2026); the repository copy entered plby/lean-proofs on 12 May 2026. The file (Lean and Mathlib v4.29.1, 856 lines) proves, for a finite simple graph on $n$ vertices with more than $\lfloor n^2/4\rfloor$ edges, the lemma $n<6\hat t$ (line 764), $\hat t$ the largest number of common neighbors of an edge, and the final theorem erdos_905 (line 840), an edge on at least $\lfloor n/6\rfloor$ triangles; the real conclusion $n/6\le t$ follows from the strict lemma, while the final theorem's floor is weaker when $6\nmid n$. Its route is not the note's: the docstring credits it to Bollobás and Nikiforov's Books in graphs, through the inequality $3\sum_vd(v)^2\le6e\hat t+2ne$ (bollobas_nikiforov, line 752). A closing comment records the axioms propext, Classical.choice and Quot.sound. No build, replay or audit of it is recorded, so the page lists no formalized evidence; the site's suffix "(LEAN)" and the community database's "proved (Lean)", as of its last update dated 7 April 2026, are catalog labels. The formal-conjectures statement file for the problem names this proof in its formal_proof attribute; it is a statement, not a formalization, and is described on the problem page.