A machine-checked proof of opacity for a Faber–Mycielski barrier
Abstract
An opaque set for the unit disc is a set meeting every straight line that meets the
disc. I report a formal verification, in Lean 4 with mathlib, that the three-piece
Faber–Mycielski barrier is opaque. The main theorem barrier_isOpaque is proved with no
sorry and depends only on the three standard axioms propext, Classical.choice,
Quot.sound; in particular the axiom audit shows no sorryAx, so no gap remains anywhere
in its dependency tree. The formalization is conditional in one explicit and deliberate
respect: the two chord parameters enter as hypotheses (the feet lie on their chords),
certified externally by interval arithmetic rather than inside the kernel. I am aware of
no prior formalization of an opaque-set result — a search of the Archive of Formal Proofs
topic listings, mathlib, and public Lean/Coq/Isabelle repositories found none — and I claim
no new bound and no optimality here, only that a specific classical opacity argument now
has a machine-checked proof. The reduction underlying it is formalized for an arbitrary
subset of the plane, not merely the disc, so it applies unchanged to squares, polygons and
any other body.
Cite it
Gonzalez, V. (2026). A machine-checked proof of opacity for a Faber–Mycielski barrier. Zenodo. https://doi.org/10.5281/zenodo.21701338