Tomas Recio, Rafael Losada and Jose Luis Valcarce. On the automatic discovery of Steiner-Lehmus generalizations

Phil Scott and Jacques Fleuriot. Idle Time Discovery in Geometry Theorem Proving

Jean Duprat. The Euclid’s plane : formalization and implementation in Coq.

Susanne Apel and Jürgen Richter-Gebert. Cancellation Patterns in Automatic Geometric Theorem Proving.

Dominique Michelucci. What is a line ?

Zou Yu and Zhang Jingzhong. Readable Machine Proofs for Particle Geometry.

Xiaoyu Chen. Formal Representation and Automated Transformation of Geometric Statements.

Pedro Quaresma. TGTP - Thousands of Geometric problems for geometric Theorem Provers.

Fadoua Ghourabi, Tetsuo Ida and Asem Kasem. Proof Documents of Origami Theorems.

Daniel Lichtblau. Midpoint locus of a triangle in a corner.

Francisco Botana, José Luis Valcarce, Miguel A. Abanades and Jesus Escribano. On performing automatic discovery in dynamic geometry environments

Sana Stojanovic, Vesna Pavlovic and Predrag Janicic. Automated Generation of Formal and Readable Proofs in Geometry Using Coherent Logic.

Tuan Minh Pham. An additional tool about the orientation for theorem proving in the Coq proof assitant

Nicolas Magaud, Agathe Chollet and Laurent Fuchs. Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective.

Laurent Fuchs and Laurent Théry. A Formalisation of Grassmann-Cayley Algebra in Coq

Pavel Pech. Equivalent formulas for a quadrilateral being cyclic

Thorsten Orendt. On the Complexity of the Reachability Problem in Dynamic Geometry.

Michael Gerhäuser and Alfred Wassermann. Automatic calculation of plane loci using Groebner bases and integration into a Dynamic Geometry System

Simon E.B. Thierry, Pascal Schreck, Pascal Mathis. Why are under-constrained systems not that bad.