What was already known
The 1988 Kajitani–Ueno–Miyano conjecture asks whether uniform density is equivalent to a cyclic basis ordering. The coprime rank-three case and paving special cases were already known.
AI involvement
Austen Fletcher directed the project. The repository attributes the main argument primarily to GPT-5.6 Sol; GPT-5.6 Sol and Claude Opus 5 prepared the original Lean and paper, with other models assisting version-2 review. Fletcher prepared the conventional presentation and audit.
The primary mathematical argument is attributed to GPT-5.6 Sol, but Fletcher directed the investigation and later revisions.
Importance
Reports the remaining divisible rank-three case; with the earlier coprime theorem, the rank-three conjecture follows.
Limitations
The Lean statement covers the divisible case only. The combination with the prior coprime theorem, non-divisible case within this artifact and higher ranks are not formalized by this theorem. A named independent human explanation of its two-gap induction is not documented.
Technical verification
Version-2 reports a successful 3058-job Lean build of rankThreeKUM with standard logical axiom dependencies and no admitted proof. The check covers the divisible rank-three theorem only; build not replayed here.
Formal checking
Lean build, theorem dependency print and admission audit
- Checker
- Lean 4 kernel in Fletcher’s pinned Mathlib development
- Scope
- rankThreeKUM: every finite uniformly dense rank-three matroid of size 3k has a cyclic basis ordering
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The conventional paper and repository describe the proof, but their disclosed drafting was AI-assisted; a named human explanation of the central mechanism is not established. Few is the evidence default.
Correction and publication history
First report of the divisible rank-three theorem.
Read this published revision