We report on a proof-checked version of Stone’s result on
the representability of Boolean algebras via the clopen sets of a totally disconnected compact Hausdorff space. Our experiment is based on a proof verifier based on set theory, whose usability can in its turn benefit from fully formalized proofs of representation theorems akin to the one discussed in this note.
