What was already known
The reported interval for V₇(16) was 28–30. Dörrer and collaborators supplied the lower bound 28; Cremer contributes the matching upper bound. The eighth-of-sixteen case remains between 28 and 29.
AI involvement
The paper’s Use of AI section states that coding assistants implemented software and drafted proofs. Cremer chose the problem, directed the searches and revised the text; no exact model identity is inferred.
Coding assistants implemented searches and drafted proofs, but no retained selection-program discovery or essential mathematical idea is individually assigned to them.
Importance
Closes one small exact-selection case by an explicit algorithm and improves other finite comparison bounds.
Limitations
The reported Lean proofs establish the new upper bounds and separate analytical lower-bound statements. The numerical lower bound 28 used for the exact optimum is prior computational work and is not recomputed in this project. The author’s independently implemented checker is not an outside researcher’s assessment. AIProofWatch has not run the search, certificate checker or Lean build.
Technical verification
A completed rigorous check is documented for the scoped statement. Jonathan Cremer project: Lean kernel and leanchecker (reported): Existence of selection programs satisfying SelectsWithin for the seven new upper bounds, including V₇(16)≤28. The imported numerical lower bound V₇(16)≥28 is outside this check.
Formal checking
Author-reported Lean kernel and leanchecker checks; not rerun by AIProofWatch.
- Checker
- Jonathan Cremer project: Lean kernel and leanchecker (reported)
- Scope
- Existence of selection programs satisfying SelectsWithin for the seven new upper bounds, including V₇(16)≤28. The imported numerical lower bound V₇(16)≥28 is outside this check.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Named human researchers explain or reconstruct the scoped central mechanism in the cited paper/account; credit for that explanation is separate from technical checking. The paper’s Use of AI section states that coding assistants implemented software and drafted proofs. Cremer chose the problem, directed the searches and revised the text; no exact model identity is inferred.
Correction and publication history
Primary-paper and pinned-artifact review, 14 October 2026. New scoped contribution; eligible for matching consented digests.
Read this published revision