All 880 Complex Realizations of the Maximal 10-Vertex Laman Graph Can Be Real
All 880 complex realizations of L880, the maximal 10-vertex Laman graph, can be real at the same time. The paper gives a computer-assisted proof, pending independent verification, that r2(L880) = r2(10) = c2(10) = 880. That settles φ10 = 1, the smallest case of Open Problem 5 in Grasegger, Koutschan and Tsigaridas (Experimental Mathematics, 2020). The best earlier result, by Bartzos, Emiris, Legerský and Tsigaridas, certified 860 and observed 868 numerically.
The certificate fixes 17 exact rational bar lengths and uses exact rational Krawczyk interval arithmetic, with no floating point, to certify 440 disjoint boxes that reflection doubles to 880. Gluing copies along the base triangle raises the certified lower bound on liminf r2(n)^(1/n) from 430^(1/7) ≈ 2.377989 to 440^(1/7) ≈ 2.385811. At Bartzos et al.'s own lengths it also certifies the lower bounds r2(L880) ≥ 868 and r3(G160) ≥ 132.
The verifiers are pure-stdlib Python. The record is a CC BY 4.0 preprint.
10.5281/zenodo.24145786 (external site)
Directed by Ahraz Arifuddin
Researched and verified by different model families across Gemini, Claude, Grok, OpenAI, and Muse