The Coq mailing list

[Christophe Bal <projetmbc AT gmail.com>]

Hello.

Is this work is available on the web ? Do you think that a mixed approach can be used ? I'm thinking of using another programming language so as to try so technic coming from statistical learning. 

Christophe BAL

Enseignant de mathématiques en Lycée et développeur Python amateur

---

French math teacher in a "Lycée" and Python amateur developer

2015-04-30 10:46 GMT+02:00 Julien Narboux <jnarboux AT narboux.fr>:

Hello,

There is currently a small team working in Strasbourg on Formal Geometry with Coq: David Braun, Gabriel Braun, Pierre Boutry, Nicolas Magaud, Pascal Schreck and myself. We are interested in foundational issues and also applications to education.

We are open to contributions from anyone. I will contact you by private mail. We have planed a phone meeting with Christopher next week.

Just for the record, the software developed by Tuan Minh Pham linking Geogebra with PCoq is a prototype which is no longer maintained. We have the source code, but I need to ask to Yves Bertot under which licence it is available. 

The current version of our library based on Tarski's axioms contains a large development (> 100kloc) in neutral geometry (the geometry without Euclid's 5th axiom: the results which are true in both euclidean and elliptic geometry) and also in euclidean geometry. It contains the construction of an ordered field from the geometric axioms as well as the synthetic proofs of some well known theorems: Pappus, Desargues,  midpoints theorem, Euler line, Varignon, ... It contains also the proof of equivalence between 10 different versions of the axiom of parallels.  We, now plan to link it to automated deduction methods (area method, Wu's method or Gröbner bases) developed previously.

Cheers,

Julien Narboux

 

2015-04-28 23:43 GMT+02:00 Christophe Bal <projetmbc AT gmail.com>:

Hello.

I am also a math teacher and I would be happy to try to contribute in such a project.

Christophe BAL

Enseignant de mathématiques en Lycée et développeur Python amateur

---

French math teacher in a "Lycée" and Python amateur developer

2015-04-28 15:23 GMT+02:00 Frédéric Blanqui <frederic.blanqui AT inria.fr>:

Hello. You may be interested by the formalization of Tarski's geometry by Gabriel Braun, Julien Narboux and Pierre Boutry. See http://dpt-info.u-strasbg.fr/~narboux/tarski.html .

Le 28/04/2015 12:23, Christopher Goyet a écrit :

Hello,

I'm looking for geometry libraries in coq, and more precisely I would be interested bythe library developed by Tuan Minh Pham. I read his thesis but I can not find the source code.
Anyone know where I could find it?

As a math teacher, i'm also interested by the interface for geometry proving with Geogebra and coq developed by Galapagos project. This project with geogebra is it still in developement? is there a way to test it ?

Thanks,

Christopher Goyet