Claims

../

2025_09_08_harris: Harris's 3-uniform hypergraph on nine vertices, the 27 transversal triples of three classes plus one triple inside a class, has 28 edges and no four vertices spanning three edges, so the statement fails at n = 3; Lean-checked.

2026_02_06_alexeev: A Lean proof found by Aristotle without a supplied proof, published by Alexeev: for every n at least 3 the complete tripartite 3-graph on 3n vertices plus one triple inside a part has n^3+1 edges and no forbidden subgraph.

---