---

Claim. Sergey Norin and Yue Ru Sun, Triangle-independent sets vs. cuts (arXiv:1602.04370v1, 14 pages), Theorem 4: for every finite simple graph $G$ on $n$ vertices,

$$\alpha_1(G)+\tau_B(G)\le\frac{n^2}{4},$$

where $\tau_B(G)$ is the least number of edges whose deletion leaves a bipartite graph, with equality exactly for joins of balanced complete bipartite graphs. Every edge set whose deletion makes $G$ bipartite meets every triangle, so $\tau_1(G)\le\tau_B(G)$ and $\alpha_1(G)+\tau_1(G)\le n^2/4$, the inequality of Problem 621, for every graph on $n$ vertices. The proof is a finite randomized partition argument with exact tuple identities and no computer input; the corpus's complete reconstruction, with four printed slips corrected, is on the source card norin_2016_triangle_independent_sets_vs_cuts and its result page theorem_4.

Depends on. Nothing in this wiki; the argument is self-contained, and the problem page's account rests on this claim.

Formalization. Lorenzo Luccioli announced on the site's thread on 19 April 2026 a Lean proof, produced with the Aristotle system, of Theorem 4 (main_inequality) and of the problem's inequality, deduced from it through tau1_le_tauB; the original is the pinned gist linked above, and the file src/latest/ErdosProblems/Erdos621.lean of Boris Alexeev's repository plby/lean-proofs, at the pinned commit linked above, carries the same proof with a header that declares it a Lean formalization of a solution of Problem 621, naming Norin and Sun as informal authors and Aristotle and Luccioli as formal authors. The final theorem is Erdos621.TriangleIndep.erdos_conjecture in the annotated port and erdos_621 in the later port, which differs from it, by whole-file comparison, only in its version header, the final theorem's name, its print-axioms command and an alias. The statement quantifies over an arbitrary finite vertex type with classical decidability, takes the greatest cardinality of an edge set meeting each triangle at most once and the least cardinality of an edge set whose removal destroys every triangle, and states $4(\alpha_1+\tau_1)\le n^2$; the equality classification is not part of it. Formal-conjectures pull request 4718, merged on 4 August 2026, links the proof as the formal_proof of its statement erdos_621, tagged research solved, and records the pull request author's correspondence check of the statement: alpha1 is the greatest cardinality on the same set, tau1 as the least number of deleted edges leaving no triangle equals meeting every triangle, and the linked theorem over an arbitrary finite vertex type covers Fin n; it records no build or axiom audit of the linked proof, and the site's label carries a Lean suffix. As the problem page records, the formal targets match the question, and the gist, the annotated solution and the later port contain no admission and no custom axiom, the printed standard-axiom list being a source comment. The corpus has not built the proof or checked its axioms, so formalized is not listed.

Acceptance. The site's curator, Thomas Bloom, records the problem as proved by this paper, after a thread comment of 13 October 2025 located it and the page was updated; the commentary states the stronger inequality the paper proves. Bujtás, Davoodi, Ding, Győri, Tuza and Yang state the stronger inequality as Theorem 2 of their refereed paper Covering the edges of a graph with triangles, Discrete Mathematics 348 (2025), 114226, citing the arXiv version and saying that it confirms the Erdős–Gallai–Tuza conjecture. That documented acceptance by the site and by named experts in refereed work is the reviewed evidence. The paper itself has no journal version located on 2026-09-05 (the arXiv record lists only v1), so refereed is not listed. The corpus's reconstruction is the project's own reading and warrants no evidence kind.