AI for mathematics

Random lines past three circles

Lines AB and BC hit the third circle equally often, for every ratio of radii in geometric progression.

Open problem settled, formally verified in Lean 4

Random lines past three circles

Random chords of two circles and a third centre

Three circles touch in a row with radii a, b, c in geometric progression. Choose A uniformly on the first circle and B, C uniformly on the second. Dan observed numerically, and asked on MathOverflow (question 499477) why, that the lines AB and BC meet the third circle with the same probability.

The paper explains it through a fact about two circles. For independent uniform points A, B on two circles whose discs have disjoint interiors, the signed offsets of the line AB from the two centres, each divided by its radius, are independent with the arcsine law (Lemma 2). The proof is a change of variables over the four pairs of points on a line, whose contributions add to a constant because the half-chords cancel. From this, Theorem 4 decides exactly which points O on the line of centres see AB and the chord BC at the same distance in distribution: O is the second centre, or the circles touch and |QO| = b(a + b)/a. This answers Dan’s question for every ratio, extends it to every circle about the third centre and to chains of circles, shows that the progression is necessary, and gives a single integral for the common hit probability.

Preprint v1, 8 October 2026, not peer reviewed. Every proved result of the paper is also formally verified in Lean 4 (lean/, standard axioms only). The exposition has not yet been independently reviewed. The author used AI tools (Claude, Anthropic; Codex, OpenAI) in this work, as described in the paper’s acknowledgements, and is responsible for its content.