The nonintersecting diagonal problem asks for the maximum number of pairwise disjoint unit-square diagonals
in an
array of squares, where is a positive integer.
Selected diagonals may neither cross nor share an endpoint.
For even , (Boyland et al. 2017). Song (2026) proved
that for odd ,
where
is the floor function. The values for , 2, ... are 1, 3, 6, 10, 16, 21, 29, 36, 46, 55, ... (OEIS
A264041).
Song (2026) reports AI assistance with the proof and Lean
formalization. The formal reduction assumes the Fisher-Fitzpatrick grid-cover theorem.
Boyland, P.; Pintér, G.; Laukó, I.; Roth, I.; Schoenfield, J. E.; and Wasielewski, S. "On the Maximum Number of Non-Intersecting
Diagonals in an Array." J. Integer Seq.20, Article 17.2.4, 2017.
https://cs.uwaterloo.ca/journals/JIS/VOL20/Pinter/pinter3.html.Fisher,
D. C. and Fitzpatrick, S. L. "The Isometric Path Number of a Graph."
J. Combin. Math. Combin. Comput.38, 97-110, 2001.Sloane,
N. J. A. Sequence A264041 in "The
On-Line Encyclopedia of Integer Sequences."Song, L. "Nonintersecting
Unit Diagonals in Odd Square Arrays." 16 Oct 2026. https://arxiv.org/abs/2610.33042.
of pairwise disjoint unit-square diagonals
in an 
array of squares, where 
is a positive integer.
Selected diagonals may neither cross nor share an endpoint.
For even 
, 
(Boyland et al. 2017). Song (2026) proved
that for odd 
,
is the floor function. The values for 
, 2, ... are 1, 3, 6, 10, 16, 21, 29, 36, 46, 55, ... (OEIS
A264041).
