Equidistant lines are a collection of distinct lines whose pairwise line-line distance is the same. For
lines in Euclidean space, this
condition is
where
and
.
For example, three parallel lines through the vertices of an equilateral
triangle perpendicular to them have this property.
In three-dimensional Euclidean space, the problem is equivalent to finding pairwise touching congruent infinite solid right circular cylinders with disjoint interiors. The axes of such cylinders have common pairwise line-line distance twice their radius. Bozóki et al. (2015) constructed seven such cylinders.
Liu (2026a) reported that eight lines in three-dimensional Euclidean space cannot have common positive pairwise line-line distance. Together with the seven-line construction, this would give a maximum of seven. The written argument combines geometric reductions with exact computations for possible configurations of directions. The project reports substantial assistance from OpenAI and Anthropic models (VibeMathed 2026).
As of Oct. 7, 2026, VibeMathed (2026) had independently rebuilt the accompanying Lean development from a clean clone and replayed it with a separate kernel checker. The formal statement excludes eight lines at common positive pairwise line-line distance, without assumptions of general position or nonparallel directions. The formalization includes the complete exclusion argument, but not the published seven-line construction or the cylinder reformulation (Liu 2026b). Independent specialist review of the mathematical statement and proof had not been reported.
The requirement that every pair of cylinders touch is different from Kuperberg's six-cylinder conjecture, which concerns cylinders touching a common unit ball.