A Formal Proof of the Banach-Tarski Theorem in ACL2(r). - Jagadish Bapanapally; Ruben Gamboa (ISAIM, 2022)

A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). - Jagadish Bapanapally; Ruben Gamboa (ITP, 2022)

A Free Group of Rotations of Rank 2. - Jagadish Bapanapally; Ruben Gamboa (ACL2, 2022)