Three circles and a fair coin

Three circles touch in pairs, and a triangle is formed by choosing one uniform random point on each. Dan asked on Mathematics Stack Exchange and MathOverflow (question 498968) why the triangle contains the incentre of the triangle of centres with probability 1/2; the equal-radius case had been done by an integral, the unequal case only by simulation.

The probability is 1/2 for all radii (Theorem 1). The key is a fact about two touching circles: a random chord joining them crosses the common tangent at a point from which the two centres are seen at an angle uniformly distributed on (π/2, π) (Theorem 2). Each side of the triangle then misses the incentre with probability equal to the opposite angle of the triangle of centres divided by 2π, and these angles sum to π. A refinement maps the pair of random points to a uniform point on a sphere, on which each miss is a lune (Theorem 3). The proof of Theorem 2 is a computation; the intuitive proof that the question asked for remains open.

Preprint v1, 9 October 2026, not peer reviewed. The algebra and calculus (chord identities, the integral equal to π, the crossing law and its distribution function, the half-angle identity, the final sum, the sphere’s folding step) are formally verified in Lean 4 (lean/, standard axioms only); the change of variables as a statement about measures and the plane geometry of Lemmas 1 and 2 are checked by hand and by simulation. The author used AI tools (Claude, Anthropic) in this work, as described in the paper’s acknowledgement, and is responsible for its content.