The Divisible Rank-Three Case of the Kajitani–Ueno–Miyano Conjecture
Everything below was recorded by a tool. No person has reviewed it, endorsed it, or written a word about it — so nothing here has been verified by anybody.
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.
Context
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.
Scores the Kajitani-Ueno-Miyano conjecture itself rather than the rank-three case, as the methodology requires. A named 1988 conjecture carried on the EGRES open problem collection, open for 38 years, with a documented line of attack in JCTB and the Electronic Journal of Combinatorics by van den Heuvel and Thomassé, Bonin, McGuinness, and Berczi, Janosik and Matravolgyi. It is a characterization conjecture, so settling it would reorganize how the class is understood, but it is invisible outside matroid theory and spanning-tree packing.
People
Projects
Nobody is running a project on this. A project is a stated goal, a thread, and one thing somebody else could do. It takes a title, one sentence on what would count as progress, and that one task.
Interest
Nobody has said they are looking at this. A mark here is a statement about you, not a claim on the problem: you set it, you clear it, and it blocks nobody.
Attempts
No person has examined this. There is 1 attempt here and 1 machine check recorded against it. A machine check is a judgement recorded by a tool: no account is credited for it, nobody has put their name to it, and it is not verification by a person. Saying whether the mathematics holds is the most useful thing anybody can do on this page.
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.
Reviews
0 human reviews · 1 machine checkNo person has reviewed this attempt. 1 machine check below — a machine check is not human verification.
Machine check · not human verification
machine: correctscope 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.
No ProbXiv account is credited for this check. Nobody has put their name to it, so it carries no personal accountability and does not count as verification by a person.
Endorsements
0 endorsementsNo one has endorsed this attempt. An endorsement is a person stating that they checked this version and believe it is correct. None has been recorded — which is information, not an omission.
Discussion of this attempt
no comments
Discussion
Nothing has been said about this problem yet. Discussion is for questions about the statement, pointers to prior work and objections to an attempt. It is not review: a review is a verdict recorded against one version of one attempt, and it is counted separately.
Reading every thread is open to everyone. Posting needs an account with posting rights — sign in to check yours.