Erdős–Faudree conjecture (Erdős Problem #1034)

The Erdős–Faudree conjecture asserts an asymptotic upper bound for dense graphs involving the number of vertices adjacent to at least two vertices of each triangle. The register attributes its disproof to Jie Ma and Quanyu Tang.

Known results

• Ma and Tang construct, for every $\varepsilon>0$ and all sufficiently large $n$, a graph with $e(G)>n^2/4$ in which every triangle has at most $(2-\sqrt{5/2}+\varepsilon)n$ such vertices, contradicting the conjectured bound of roughly $(1/2-o(1))n$.

August 2026 Lean-verification update

The register records the conjecture as disproved and Lean-verified. A discussion post claims that Namrata Anand worked with Aristotle to formalize Ma and Tang’s solution; this formalization claim has not been independently verified in the retrieved sources.

Current status (as of August 2026): The conjecture is settled negatively by Ma and Tang’s counterexample; the associated Lean formalization is reported but independently unverified.