The Divisible Rank-Three Case of the Kajitani–Ueno–Miyano Conjecture
The Kajitani–Ueno–Miyano conjecture asserts that every finite uniformly dense matroid has a cyclic basis ordering. The conjecture is proved for all matroids of rank three. The new result establishes the previously unresolved divisible case, where the ground-set size is a multiple of three, without assumptions of simplicity, representability or paving. Together with the previously published coprime-case theorem of van den Heuvel and Thomassé, this covers every finite uniformly dense rank-three matroid. The unrestricted conjecture remains open in higher rank.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Matroid theory
- Posed by
- Kajitani, Ueno and Miyano
- Year posed
- 1988
- Years open
- 38y
- Solved
- 2026-08-05
- Model
- GPT-5.6 Sol; Claude Opus 5 (for some Lean formalization and paper write-up)
- Vendor
- OpenAI; Anthropic
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 30 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Proves the divisible rank-three case: rank exactly three and ground-set size a multiple of three, with no restriction to simple, paving, representable or graphic matroids. The part not previously in the literature is the non-simple sub-case, since McGuinness had settled all paving matroids and a rank-three matroid is paving exactly when it has no parallel pairs. Combined with the coprime-case theorem of van den Heuvel and Thomasse, this covers every finite uniformly dense rank-three matroid. The conjecture remains open in higher rank.
What the AI did
Under human direction, GPT-5.6 Sol developed the central mathematical argument, including the tight-set reduction, the universal two-gap insertion theorem, and the deletion-and-induction treatment of the strictly dense case. GPT-5.6 Sol and Claude Opus 5 then collaboratively produced the Lean 4 formalization and the accompanying mathematical paper. Human oversight directed the project, selected and evaluated proof directions, coordinated the formal verification, and checked the scope and relation to the existing literature.
Verification
The new divisible rank-three theorem is formalized end to end in Lean 4. The repository builds successfully with 3,046 jobs, zero errors and zero warnings. The principal theorem contains no sorry, admit, custom axiom declaration, unsafe declaration or use of native_decide; Lean reports only the standard Mathlib axioms propext, Classical.choice and Quot.sound. The conclusion for all rank-three matroids additionally invokes the published coprime-case theorem of van den Heuvel and Thomassé, which is not formalized in this repository. The divisible ingredient is therefore Lean-verified, and the complete rank-three result is established modulo that named literature theorem. This is a complete resolution in rank three but a partial result toward the unrestricted Kajitani–Ueno–Miyano conjecture, which remains open in higher rank. The manuscript is an unrefereed Zenodo preprint.
Sources
Cyclic basis orderings of uniformly dense rank-three matroids
Submitted by HiddenHawk615