What was already known
Li and Liang’s v2 theorem asserted an arithmetic-progression classification when |A|+|B|≤p−1. Their stated exception families lie on the boundary |A|+|B|=p.
AI involvement
AI search found the Z/13 pair and built its Lean certificate in a human-maintained audit project.
AI found the retained counterexample and built its certificate within a human-maintained audit project.
- Supporting source (github.com) — counterexample_main and counterexample_lemma declarations
Importance
Gives a concrete counterexample within the claimed non-boundary range of a recent inverse theorem.
Limitations
The correction applies to version 2 of the Li–Liang preprint. A separate Z/11 witness against Lemma 3.2 needs its own assessment. The repository reports no independent human expert review; AIProofWatch independently enumerated the Z/13 sums and progressions.
Technical verification
The source reports a complete kernel-reduced finite certificate of the exact Z/13 arithmetic conditions, restricted sumset and non-progression. AIProofWatch independently enumerated the Z/13 and Z/11 sumsets and tested all cyclic arithmetic progressions.
Formal checking
Lean 4 decide +kernel exact finite-set computation. RestrictedSumsetsAudit.counterexample_main: Z/13 witness and all stated hypotheses
- Checker
- Lean 4 kernel
- Scope
- In ℤ/13ℤ, A={0,1,3,4,5,6,10} and B={0,1,4,6} have |A|+|B|=11≤12. Their restricted sumset is {1,3,4,5,6,7,9,10,11}, of size 9=|A|+|B|−2, but neither A nor B is an arithmetic progression. This contradicts the forward conclusion of Li–Liang Theorem A/3.1 in arXiv:2609.10148v2.
- Basis
- Reported by the linked checker
exhaustive integer modular enumeration of restricted sums and all cyclic arithmetic progressions. The stated Z/13 restricted sumset has nine residues and neither set is a cyclic arithmetic progression; the Z/11 lemma witness has five residues
- Checker
- AIProofWatch batch 14 review
- Scope
- In ℤ/13ℤ, A={0,1,3,4,5,6,10} and B={0,1,4,6} have |A|+|B|=11≤12. Their restricted sumset is {1,3,4,5,6,7,9,10,11}, of size 9=|A|+|B|−2, but neither A nor B is an arithmetic progression. This contradicts the forward conclusion of Li–Liang Theorem A/3.1 in arXiv:2609.10148v2.
- Basis
- Reproduced by AIProofWatch
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The explicit sets, nine sum residues and failed progression conclusion make the mechanism human-readable; the source explains the comparison clause by clause.
Correction and publication history
The Z/13 theorem counterexample is distinct from the separate Z/11 lemma witness.
Read this published revision