EasyChair Smart Slide
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)