---

The claim. For every $n\ge3$, the $3$-uniform hypergraph on the $3n$ vertices $\{0,1,2\}\times\{0,\dots,n-1\}$ whose edges are the $n^3$ triples with one vertex in each part together with the triple $\{(0,0),(0,1),(0,2)\}$ inside the first part has at least $n^3+1$ edges, no four vertices spanning three edges and no five vertices spanning seven. So the statement of Problem 794 fails for every $n\ge3$, and the answer to the question as written is no. The result is the theorem construction_properties of the Lean file src/v4.24.0/ErdosProblems/Erdos794c.lean in Boris Alexeev's lean-proofs repository (plby/lean-proofs), linked above at the commit of 15 September 2026 (Lean and Mathlib v4.24.0). Alexeev's comment of 5 February 2026 on the site's discussion thread, which announces the Lean check of Harris's example, adds in a later update (the file it links was first committed on 6 February 2026) that Aristotle proved the result by itself without a proof provided, using essentially the same example, and links this file. The file carries no informal-author header: it states the construction and proves its properties in Lean, so it is an independent proof by an AI system, published by Alexeev, and has its own page; the Lean checks of Harris's example are links on Harris's page.

The file's construction_properties n (h : 3 ≤ n) asserts, for construction n (the union of tripartite_edges n and extra_edges n, the latter empty when $n<3$), that every edge has three vertices, that the edge count is at least n^3 + 1, and that there is no vertex set of size $4$ spanning at least $3$ edges and none of size $5$ spanning at least $7$; its closing comment records #print axioms as propext, Classical.choice and Quot.sound. The theorem states the construction's properties for each $n\ge3$ and does not itself negate the problem's quantified statement; the negation follows by instantiating any $n\ge3$. The hypothesis $3\le n$ is needed, since a part with fewer than three vertices holds no triple.

Depends on. Nothing in this wiki: the construction and its verification are the file's own.

Acceptance. None recorded. The corpus has not built or audited the file and holds no statement-fidelity audit of it, so formalized is not listed; no outside reviewer is recorded for this file, and the site's label DISPROVED (LEAN) and the formal-conjectures formal_proof attribute both name the Lean check of Harris's example, not this file. No journal publication exists and none is expected. The claim stays claimed; the problem's standing rests on the accepted page of Harris.