Partial proof of the Kasami APN triple-count conjecture, verified in Lean
A conjecture from a 2019 cryptography olympiad on triple counts for the Kasami almost perfect nonlinear function is proved in four residue cases and verified exhaustively for small field degrees, with every proof machine-checked.
- Lab
- Independent
- Model
- Claude Fable 5; Harmonic Aristotle
- Field
- Mathematics
- Date
- 2026-08-19
- Human collaborators
- Gábor P. Nagy, Attila Vajda
- Problem posed
- 2019 · open 7 yrs
Sources
Original work
Independent commentary
What was found
For the Kasami almost perfect nonlinear function on a binary field, the conjecture concerns a set built from the function's second difference and asserts that, for any two distinct nonzero elements, the number of triples in that set satisfying a fixed linear relation is exactly 2^(2n-3). The paper proves this when k modulo n lies in the set {1, 2, n-2, n-1}, including a complete proof for k = 2 via quadratic-form theory and an exact root-count reduction, and verifies the conjecture exhaustively by computer for every admissible pair with n at most 13. It also corrects one hypothesis in the supporting facts supplied with the original problem, concerning the Müller-Cohen-Matthews permutation.
Novelty check
The conjecture was proposed at the NSUCRYPTO 2019 cryptographic olympiad, with the proposer not publicly disclosed, and the companion repository supplied with the problem records which supporting facts were already formally verified, so the starting point is unusually well defined. Working from that inventory the authors identify one hypothesis in it as essential and correct it, which is itself evidence the prior material was checked rather than assumed. The result is a partial proof of an open conjecture, not a retrieval.
Caveats and known objections
A preprint, unrefereed, with no independent human check on record, and the result is explicitly partial: four residue classes of k modulo n plus exhaustive verification for n at most 13, not the conjecture. The formal grade rests on the authors' statement that all new results and proofs have been formally verified in Lean 4 by Aristotle from Harmonic, with provenance details in the acknowledgements; vibemathed records the Lean development as checked with its statement unaudited, so nobody outside has confirmed the formalized statements match the paper. Autonomy is graded ai-led on a strong and specific disclosure: every proof in the paper was obtained by prompting Claude Fable 5 with the conjecture statement, background hints and a pointer to the companion repository, and the human authors supplied the framing and the subsequent verification.
Also recorded at
vibemathedkasami-apn-function-triple-count-conjecture
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Partial proof of the Kasami APN triple-count conjecture, verified in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-19-kasami-apn-triple-countsBibTeX
@misc{whataifound-independent-2026-counts,
title = {Partial proof of the Kasami APN triple-count conjecture, verified in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-08-19-kasami-apn-triple-counts}
}