coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Banach-Tarski paradox in Coq (proof completed)

From: 永江哲朗 <tetsuro.nagae AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Banach-Tarski paradox in Coq (proof completed)
Date: Mon, 17 Apr 2017 18:05:19 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tetsuro.nagae AT gmail.com; spf=Pass smtp.mailfrom=tetsuro.nagae AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f170.google.com
Ironport-phdr: 9a23:fRrngB/orNoktP9uRHKM819IXTAuvvDOBiVQ1KB41+4cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRx3miCkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTypDAIW6bYkJEuEMOvpYoJfhp1sVsBu+Hw6sCPnpyjBSiX/5x7M13v8uEQHDxgMgHtYOvG7Io9XyMacfSOa4x7TGwzXEavNZwzb96I7QfxAgp/GMR7NwftDLxUkhDQPJllqQqY35PzOVy+QCqHKX4PZnVeKqjWMstgJ/oiC3y8syloXEgpgZx1PE+Clj3Yo5O961RFRmbdOmDJddsTyROZFsTcM4WW5ovT43yr0Ytp6/eygH0JEnyATea/yDaoSJ7AjjWPqILTd2mX5oeq6ziwy98Uinze38Wc2030hQoiVZldnMs2gB1x3V6seZVvtw5lmt1SqL2gzJ6exJIVo4mbfFJ5Mi2LI8i5gevVjbEi/zgkr2jauWdks++uiv7uTqeqnmqYGAN49vlwH+KKMulta5AesiPQgBRXaU9P+z1L3m50L5QbFKgucqnanetZDWPd4bqbKhAw9JzoYj7A6yACuh0NQBhHUIMFZFeA+cgIXyIFHPIPX4De+ljFi2kTdrwerGPrz7DZnXIHjDiuSpQbEo4ElFjQE30Np35pROC7hHLuigdFX2sYkg9ufBe1iozvr8Fc96kIUXVmuCKqCcOaLW91SP47R8cKG3eIYJtWOleLAe7Pn0gCphlA==

Thank you for your sharing.

We talked about your proof at our small coq study group last Saturday.

I'd like to read your proof through and understand it.

Now I'm reading a book which explains Banach-Tarski paradox.

Thanks.

2017-04-12 9:44 GMT+09:00 Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>:

Hi all,

Banach-Tarski paradox translated into Coq. Just completed.

Sources accessible here:
https://github.com/roglo/banach_tarski

Enjoy!

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] Banach-Tarski paradox in Coq (proof completed), Daniel de Rauglaudre, 04/12/2017
- Re: [Coq-Club] Banach-Tarski paradox in Coq (proof completed), 永江哲朗, 04/17/2017
  - Re: [Coq-Club] Banach-Tarski paradox in Coq (proof completed), Daniel de Rauglaudre, 04/17/2017