The Kajitani-Ueno-Miyano conjecture (Kajitani et al. 1988) states that a finite matroid admits a cyclic basis ordering iff it is a uniformly dense matroid.
Van den Heuvel and Thomassé (2012) proved the conjecture when the cardinality 
of the ground set and the
matroid rank 
are relatively prime.
Fletcher (2026a) reported a proof of the remaining case
of matroid rank 3, in which 
is divisible by 3. His theorem states that for every positive
integer 
, every finite uniformly
dense matroid of matroid rank 3 on 
elements admits a cyclic
basis ordering. Together, the two results give the claimed conclusion for all
finite matroids of matroid
rank 3.
Fletcher (2026a) credits GPT-5.6 Sol with developing the central argument under his direction. GPT-5.6 Sol and Claude Opus 5 produced the original Lean 4 formalization
and manuscript, while GPT-6 Astra and Fable 5.1 assisted the review and refinement
of version 2. The theorem for 
divisible by 3 is formalized
end-to-end in Lean 4 (Fletcher 2026b). The published theorem
for the relatively prime case used to obtain
the full conclusion is not formalized there. As of Sep. 11, 2026, no independent
specialist verification or peer review of the new argument had been reported (VibeMathed
2026). The general conjecture remains open for higher
matroid ranks.
Elements Are Independent." Disc. Math. 72,
187-194, 1988.