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.
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.