The Divisible Rank-Three Case of the Kajitani–Ueno–Miyano Conjecture
Statement
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.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
GPT-5.6 Sol; Claude Opus 5 (for some Lean formalization and paper write-up)The record names only the tool that produced this, and no ProbXiv account is credited for it.
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.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
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.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.