All Projects → roglo → banach_tarski

roglo / banach_tarski

Licence: other
Formal proof in Coq of Banach-Tarski paradox.

Programming Languages

Coq
218 projects
Banach-Tarski paradox.

Inspirations:
   - Stan Wagon: The Banach-Tarski Paradox, Cambridge University Press
   - Wikipedia: Banach–Tarski paradox
   - http://people.math.umass.edu/~weston/oldpapers/banach.pdf

Compilable with Coq v8.14
Author: Daniel de Rauglaudre

Started: Wed Jul 20 17:16:53 2016 +0200
Proof completed: Tue Apr 11 11:08:19 2017 +0200.
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].