A short open space curve of unit width
Tinko Sebastian Bartels, Dennis Kevin Choy, Ruixiang Wu, Tongxin Li
math.MG
Oct 14, 2026 · v1
math.DG
TL;DR
Supplies a Lean 4 formalization (using Mathlib and LeanCert) of the curve's length bounds, local minimality, and interval-arithmetic width certificate, generated with AI assistance.
Abstract
In this work, we propose a curve to be a minimum of length among rectifiable, continuous curves of unit width in three-dimensional Euclidean space. We show that a previously conjectured minimizer of that problem is not of unit width, give the numerical derivation of a candidate family of unit width curves, prove that it admits a strict local minimum within that candidate family and that this minimum is of unit width and length $3.905124162243593\ldots$. The curve consists of eight straight segments, two cone geodesics, and three circular helices. Its parameters are specified by a uniquely isolated solution of the joining and stationarity equations. To establish unit width in every direction, we combine analytic estimates with interval arithmetic on a finite covering of the remaining directions. We conjecture that the curve is globally minimizing. We supplement this work with the programs used to identify the candidates, replicate the computer-assisted parts of our proof, as well as a formalization of our proof in Lean.
Problem
The task is to find a shortest rectifiable open curve of unit width in three-dimensional Euclidean space. Zalgaller's conjectured minimizer L_3, of length about 3.9215, turns out not to have unit width.
Approach
Numerical sequential convex optimization over polygonal chains suggests a candidate shape. The resulting curve has eight segments, two cone geodesics and three circular helices, and its parameters come from joining and stationarity equations. Unit width in every direction is established by combining analytic estimates near critical directions with interval arithmetic over 512 cone-subdivision leaf checks. The proof is formalized in Lean 4 with Mathlib and LeanCert, using only standard axioms, alongside independent mpmath certificates.
Results
The curve has unit width and length 3.905124162243593..., and it is a strict local minimum within the candidate family. The Lean proof verifies the main result with slightly looser bounds, 3.90512404 < L < 3.90512429. Global minimality is conjectured, and an improved closed-curve bound of about 5.0944 is also reported.
