---

The claim. Let $A=\{1,2,3\}$, $B=\{4,5,6\}$ and $C=\{7,8,9\}$, and let $H$ be the $3$-uniform hypergraph on $\{1,\dots,9\}$ whose edges are the $27$ triples with one vertex in each of $A$, $B$, $C$ and the triple $A$. Then $H$ has $3^3+1=28$ edges on $3\cdot3$ vertices, no four of its vertices span three edges, and therefore (since five vertices spanning seven edges would contain four spanning three) no five of its vertices span seven. The statement of Problem 794 fails at $n=3$, so the answer to the question as written is no. The same construction, the complete $3$-partite $3$-graph with classes of size $n$ plus one triple inside a class, fails the statement for every $n\ge3$ (a class needs three vertices to hold the extra triple). The site credits the example to Phillip Harris and thanks them, without a date; this page is dated by the earliest dated record of the credit, an archived copy of the site's page of 8 September 2025, which already carries the example, the label DISPROVED and the thanks to Harris; an archived copy of 12 February 2025 shows the problem OPEN without the commentary, and the site's revision history holds the example in its earliest stored revision, of 20 October 2025. The thread comment of 5 February 2026 reports the example's formalization, and the site records that it was updated in response.

The site's commentary reads the statement as a misprint for the Turán density of $K_4^-$ (four vertices spanning three edges); the problem page judges the statement as printed and records that reading as a variant with its own answer.

The formalization. Boris Alexeev reports in the site's discussion thread (5 February 2026) that the counterexample was formalized in Lean by the direct finite check, with a decide proof whose axioms are propext, Classical.choice and Quot.sound, and a faster variant using native_decide; a later update to the comment adds that Aristotle proved the result by itself without a supplied proof, with essentially the same example, which is an independent proof with its own page. The three files linked above, at the commit of 15 September 2026 of Alexeev's lean-proofs repository (plby/lean-proofs), each declare themselves a Lean formalization of a solution to Problem 794 formalizing Harris's explicit counterexample: src/v4.29.1/ErdosProblems/Erdos794.lean (Lean and Mathlib v4.29.1; 84 lines) names Phillip Harris as informal author and Aristotle, ChatGPT and Boris Alexeev as formal authors, and the two files under src/v4.24.0/ (Lean and Mathlib v4.24.0) say that Aristotle and ChatGPT were used, Erdos794b.lean proving the finite check by native_decide (axioms including Lean.ofReduceBool and Lean.trustCompiler) and Erdos794.lean by decide. The v4.29.1 file defines the three classes, the $27$ transversal triples and the extra edge $\{1,2,3\}$, proves by decide that every edge has three elements, that there are at least $3^3+1$ edges and that no four vertices span three edges and no five span seven, and derives the negation of its own predicate erdos_794 (for every $n$, every $3$-uniform edge set on a vertex set of size $3n$ with at least $n^3+1$ edges has a $(4,3)$ or a $(5,7)$ subgraph) by instantiating $n=3$. The formal-conjectures statement of the problem is tagged research solved with a formal_proof attribute naming the v4.29.1 file on its repository's main branch, unpinned; the problem page's Formalization section describes that statement file, whose own erdos_794 keeps sorry while, since 18 September 2026, its harris variant proves the same finite check by decide +kernel. The statement file is not linked here: a formal-conjectures statement file is not a formalization link, and the problem page records the kernel-checked variant. The problem page also records two observations of the corpus's own: the v4.29.1 file's predicate searches for the forbidden subgraphs inside the fixed nine-element set rather than inside the general vertex set, so it is not a literal transcription of the formal-conjectures statement, though for the counterexample, whose edges all lie in that set, the refutation is sound; and the collection's harris variant states the same finite check with the vertices shifted by one. The v4.29.1 file contains no sorry, axiom, native_decide or unsafe; the corpus has not built or audited any of the three files and holds no statement-fidelity audit of them, so formalized is not listed.

Recomputation. The example is stated in the site's commentary and the check is elementary. The problem page recomputes it (the pattern count of a four-vertex set against the three classes, and the double count showing that seven edges on five vertices force three on four); that recomputation is the corpus's own and warrants no evidence kind.

Acceptance. Reviewed: the site's curator, T. F. Bloom, records the example in the problem's commentary as an elementary refutation of the statement as written, thanks Harris, and labels the problem DISPROVED (LEAN) with a gloss saying the problem is solved in the negative and the proof verified in Lean (erdosproblems.com/794, as of 2026-09-18 and 2026-10-07); the community database lists the problem as disproved (Lean) as of its last update on 5 February 2026, and the statement as formalized since 4 August 2026; formal-conjectures names the Lean file as the problem's formal proof. The site marks thread comments as unverified. No journal publication exists and none is expected for a finite check.