1 Search Results for "Bapanapally, Jagadish"


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

Authors: Jagadish Bapanapally and Ruben Gamboa

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


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.

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)


Copy BibTex To Clipboard

@InProceedings{bapanapally_et_al:LIPIcs.ITP.2022.5,
  author =	{Bapanapally, Jagadish and Gamboa, Ruben},
  title =	{{A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.5},
  URN =		{urn:nbn:de:0030-drops-167142},
  doi =		{10.4230/LIPIcs.ITP.2022.5},
  annote =	{Keywords: ACL2(r), Banach-Tarski, Rotations}
}
  • Refine by Author
  • 1 Bapanapally, Jagadish
  • 1 Gamboa, Ruben

  • Refine by Classification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 ACL2(r)
  • 1 Banach-Tarski
  • 1 Rotations

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail