| 71 | -- | 72 | Pascal Schreck, Tetsuo Ida, Laura Kovács. Foreword - Formalization of geometry, automated and interactive geometric reasoning |
| 73 | -- | 87 | Zoltán Kovács, Tomás Recio, Csilla Sólyom-Gecse. Rewriting input expressions in complex algebraic geometry provers |
| 89 | -- | 117 | Sana Stojanovic Durdevic. From informal to formal proofs in Euclidean geometry |
| 119 | -- | 146 | Mladen Nikolic, Vesna Marinkovic, Zoltán Kovács, Predrag Janicic. Portfolio theorem proving and prover runtime prediction for geometry |
| 147 | -- | 173 | Jean-Philippe Pernot, Dominique Michelucci, Marc Daniel, Sebti Foufou. Towards a better integration of modelers and black box constraint solvers within the product design process |
| 175 | -- | 192 | Ariel Kellison, Mark Bickford, Robert L. Constable. Implementing Euclid's straightedge and compass constructions in type theory |
| 193 | -- | 212 | David Braun, Nicolas Magaud, Pascal Schreck. Two cryptomorphic formalizations of projective incidence geometry |
| 213 | -- | 257 | Michael Beeson, Julien Narboux, Freek Wiedijk. Proof-checking Euclid |
| 259 | -- | 291 | Johann A. Makowsky. Can one design a geometry engine? - On the (un)decidability of certain affine Euclidean geometries |