#### Incremental Convex Hull Algorithm in 2D

#### Delaunay triangulation

Jean-François Dufourd and Yves Bertot proposed a formal description of an algorithm to transform an arbitrary triangulation into a Delaunay triangulation by successive flips. It is available here and is verifiable with Coq-8.2, extended with csdp for the

psatz tactic. A port of this development for Coq-8.5 is now available.#### Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective

Nicolas Magaud, Agathe Chollet and Laurent Fuchs currently work on a formalization of the Harthong-Reeb line in Coq. The Coq definitions and proofs are available here. It is a work in progress and shall be updated when new results are obtained.#### Hypermaps, Genus theorem and Euler formula

Jean François Dufourd proposed a Coq development about hypermaps and the formalization of the Genus theorem and the Euler formula. It is available as a user contributions of Coq.#### Geometric Algebras

Laurent Fuchs and Laurent Théry proposed a Coq development for Geometric Algebras.#### Ruler and Compass geometry

Jean Duprat developed an axiom system for ruler and compass geometry. It is available as a user contribution of Coq.

This library contains an axiomatization of the ruler and compass euclidian geometry. Files A1 to A6 contain the axioms and the basic constructions. The other files build the proof that this axiomatization induces the whole plane geometry except the continuity axiom. For that the proofs of the Hilbert's axioms conclude this work in the files E1 to E5.#### Highschool's geometry

Frédérique Guilhot proposed a Coq development about high-school geometry in Coq. It is available as a user contributions of Coq or on her page.

#### Tarski's geometry

Julien Narboux proposed a Coq development about Tarski's geometry in Coq. It is available as a user contributions of Coq or on his page.

#### Projective Geometry

Nicolas Magaud, Julien Narboux and Pascal Schreck proposed a Coq development about projective geometry in Coq. It is available as a user contributions of Coq or on this page.

Christophe Brun, Jean-François Dufourd et Nicolas Magaud formalized a incremental algorithm to compute convex hulls of points in the plane. They use hypermaps as their data structure to represent objects and carried out the proofs using the Coq proof assistant. Formal development (in gallina)

#### Area method

Julien Narboux proposed a formalization of the area method in Coq. It is available as a user contributions of Coq or on his page.