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.
Gonzalez, V. (2026). A machine-checked proof of opacity for a Faber–Mycielski barrier. Zenodo. https://doi.org/10.5281/zenodo.21701338