What was already known
Alon had disproved the Körner–Simonyi equality C(T)=t(T), including a 67-vertex Paley tournament, and asked for the smallest counterexample. The repository notes that 26- and 27-vertex examples can be derived from published finite-field arguments; no prior seven-vertex example was found in its bounded search.
AI involvement
JD Jones directed the project. The disclosure says Claude produced the computations, searches, proofs, checkers and repository, including the vertex-deletion search that found T₇; this documents central AI mathematical work.
The disclosure states JD Jones directed the project while Claude produced the search, computations, proofs and repository; the vertex-deletion search found the retained T₇ witness.
Importance
Determines the minimum order and supplies a concrete seven-vertex witness, with a formal finite classification excluding smaller tournaments.
Limitations
The Lean claims do not prove that this is the unique seven-vertex counterexample, the exact capacity of T₇, or equality of the supremum and limit definitions; those stronger statements have separate finite certificates or cited background. No independent human review is reported. Local Lean and exact-certificate checks are source-reported; novelty beyond the bounded literature search remains open.
Technical verification
The source reports all 19 selected Challenge statements proved in Solution with a Lean axiom audit, kernel-checked finite coverage and exact certificate cross-checks. Formal applies to the selected minimal-order witness and six-vertex exclusion, not to uniqueness at order seven or exact capacity.
Formal checking
All 19 selected statements have completed Lean proofs, a source-reported axiom audit and kernel-checked finite coverage; separate Python certificates cross-check finite witness data.
- Checker
- Lean 4 kernel and documented comparator/certificate checks run by the repository authors
- Scope
- Let T₇ be the tournament induced by residues 0,1,2,3,9,14,18 in the Paley tournament modulo 23. Its largest transitive subtournament has order 4, while its Sperner capacity satisfies √18≤C(T₇)≤5 and is therefore greater than 4. Every tournament on at most six vertices has C(T)=t(T), so seven is the least possible order of such a counterexample. Capacity is formalized as a supremum of finite-power rates.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The source reports no independent human mathematical review or explanation of the central witness search. Few is the evidence default.
Correction and publication history
Primary-source review of the exact T₇ witness, six-vertex exclusion, AI search disclosure and limits of the formal proof.
Read this published revision