Document

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

## File

LIPIcs.ITP.2022.5.pdf
• Filesize: 0.65 MB
• 15 pages

## Acknowledgements

We want to thank professor John Cowles at the University of Wyoming for assisting us in the proof verifying the denumerability of the poles.

## Cite As

Jagadish Bapanapally and Ruben Gamboa. A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.5

## Abstract

This paper presents a formal proof of the Banach-Tarski theorem in ACL2(r). The Banach-Tarski theorem states that a unit ball can be partitioned into a finite number of pieces that can be rotated to form two identical copies of the ball. We have formalized 3D rotations and generated a free group of 3D rotations of rank 2. In prior work, the non-denumerability of the reals was proved in ACL2 (r), and a version of the Axiom of Choice that can consistently select a representative element from an equivalence class was introduced in ACL2 version 3.1. Using the free group of rotations, and this prior work, we show that the unit sphere can be decomposed into two sets, each equivalent to the original sphere. Then we show that the unit ball except for the origin can be decomposed into two sets each equivalent to the original ball by mapping the points of the unit ball to the points on the sphere. Finally, we handle the origin by rotating the unit ball around an axis such that the origin falls inside the sphere. Seemingly paradoxically, the construction results in two copies of the unit ball.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Logic and verification
##### Keywords
• ACL2(r)
• Banach-Tarski
• Rotations

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Piergiorgio Bertoli and Paolo Traverso. Design Verification of a Safety-Critical Embedded Verifier, pages 233-245. Kluwer Academic Publishers, USA, 2000.
2. John Cowles and Ruben Gamboa. Using a first order logic to verify that some set of reals has no lesbegue measure. In International Conference on Interactive Theorem Proving, pages 25-34. Springer, 2010.
3. Ruben Gamboa. Mechanically Verifying Real-Valued Algorithms in ACL2. PhD thesis, Citeseer, 1999.
4. Ruben Gamboa and John Cowles. A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. In International Conference on Interactive Theorem Proving, pages 51-66. Springer, 2012.
5. Ruben Gamboa, John Cowles, and JV Baalen. Using ACL2 Arrays to Formalize Matrix Algebra. In Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2’03), volume 1, 2003.
6. Ruben A. Gamboa and Matt Kaufmann. Nonstandard Analysis in ACL2. J. Autom. Reason., 27(4):323-351, November 2001. URL: https://doi.org/10.1023/A:1011908113514.
7. Thomas J Jech. The Axiom of Choice. Courier Corporation, 2008.
8. J. Strother Moore. Milestones from the pure lisp theorem prover to acl2. Form. Asp. Comput., 31(6):699-732, December 2019. URL: https://doi.org/10.1007/s00165-019-00490-3.
9. Rotation matrix. Rotation matrix - Wikipedia, the free encyclopedia. https://en.wikipedia.org/wiki/Rotation_matrix, 2021. Online; Accessed: 2022-02-04.