1. Dušan Djuki\'c, Vladimir Jankovi\'c, Ivan Mati\'c & Nikola Petrovi\'c (2011): The IMO compendium, second edition. Springer, New York, doi:10.1007/978-1-4419-9854-5.
  2. Manuel Eberl (2019): Selected Problems from the International Mathematical Olympiad 2019. Archive of Formal Proofs., Formal proof development.
  3. Jean-David Génevaux, Julien Narboux & Pascal Schreck (2011): Formalization of Wu's Simple Method in Coq. In: Jean-Pierre Jouannaud & Zhong Shao: Certified Programs and Proofs. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 71–86, doi:10.1007/978-3-642-25379-9_8.
  4. Predrag Janiči\'c, Julien Narboux & Pedro Quaresma (2012): The Area Method: a Recapitulation. Journal of Automated Reasoning 48(4), pp. 489–532, doi:10.1007/s10817-010-9209-7. Available at
  5. Tobias Nipkow (2020 (accessed Jun 20, 2020)): Programming and Proving in Isabelle/HOL. Available at
  6. Tuan-Minh Pham, Yves Bertot & Julien Narboux (2011): A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Beniamino Murgante, Osvaldo Gervasi, Andrés Iglesias, David Taniar & Bernady O. Apduhan: Computational Science and Its Applications - ICCSA 2011. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 368–383, doi:10.1007/978-3-642-21898-9_32.
  7. Sana Stojanovi\'c-\begingroupłet [Pleaseinsert\PrerenderUnicode├Éintopreamble]ur\IeCđ evi\'c (2019): From informal to formal proofs in Euclidean geometry. Annals of Mathematics and Artificial Intelligence 85(2), doi:10.1007/s10472-018-9597-7. Available at
  8. Freek Wiedijk (2006): The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence). Springer-Verlag, Berlin, Heidelberg, doi:10.1007/s11225-007-9093-2.

Comments and questions to:
For website issues: