The double-cap conjecture asserts that a measurable set on the unit hypersphere 
containing no orthogonal pair of vectors
has normalized area no larger than two opposite open spherical
caps of angular radius 
. For 
, the proposed bound is
 |
where 
and 
is the gamma function. The caps are open so their
union contains no orthogonal pair.
Ibiapina et al. (2026) reported a proof for completed-measurable sets, with equality forcing agreement almost everywhere with two such opposite caps. They also report a separate AI-assisted Lean proof based on a different argument. That formalization is not a verification of the paper's own argument or of all its additional results. Neither complete proof has been independently checked here.
and the Double-Cap Conjecture." 20 Oct 2026.