Skip to Content.

Sympa Menu

coq-club - [Coq-Club] Banach-Tarski paradox in Coq (proof completed)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Banach-Tarski paradox in Coq (proof completed)
Date: Wed, 12 Apr 2017 02:44:24 +0200

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

Archive powered by MHonArc 2.6.18.