@book(imocompendium,
 author       = {Du\v{s}an Djuki\'{c} and Vladimir Jankovi\'{c} and Ivan Mati\'{c} and Nikola Petrovi\'{c}},
 year         = {2011},
 title        = {The IMO compendium},
 edition      = {second},
 publisher    = {Springer},
 address      = {New York},
 doi          = {10.1007/978-1-4419-9854-5},
)
@article(IMO2019-AFP,
 author       = {Manuel Eberl},
 year         = {2019},
 title        = {Selected Problems from the International Mathematical Olympiad 2019},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/IMO2019.html}, Formal proof development},
)
@inproceedings(wucoq,
 author       = {Jean-David G{\'e}nevaux and Julien Narboux and Pascal Schreck},
 year         = {2011},
 title        = {Formalization of Wu's Simple Method in Coq},
 editor       = {Jean-Pierre Jouannaud and Zhong Shao},
 booktitle    = {Certified Programs and Proofs},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {71--86},
 doi          = {10.1007/978-3-642-25379-9_8},
)
@article(areamethod,
 author       = {Jani\v{c}i\'{c}, Predrag and Julien Narboux and Pedro Quaresma},
 year         = {2012},
 title        = {{The Area Method: a Recapitulation}},
 journal      = {{Journal of Automated Reasoning}},
 volume       = {48},
 number       = {4},
 pages        = {489--532},
 doi          = {10.1007/s10817-010-9209-7},
 url          = {http://hal.archives-ouvertes.fr/hal-00426563},
)
@manual(isabelle-prog-prove,
 author       = {Tobias Nipkow},
 year         = {2020 (accessed Jun 20, 2020)},
 title        = {Programming and Proving in Isabelle/HOL},
 url          = {http://isabelle.in.tum.de/doc/prog-prove.pdf},
)
@inproceedings(geocoq,
 author       = {Tuan-Minh Pham and Yves Bertot and Julien Narboux},
 year         = {2011},
 title        = {A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry},
 editor       = {Beniamino Murgante and Osvaldo Gervasi and Andr{\'e}s Iglesias and David Taniar and Bernady O. Apduhan},
 booktitle    = {Computational Science and Its Applications - ICCSA 2011},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {368--383},
 doi          = {10.1007/978-3-642-21898-9_32},
)
@article(informaltoformal,
 author       = {Stojanovi\IeC{\'c}-\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{Ð}intopreamble]ur\IeC{\dj}evi\IeC{\'c}, Sana},
 year         = {2019},
 title        = {{From informal to formal proofs in Euclidean geometry}},
 journal      = {{Annals of Mathematics and Artificial Intelligence}},
 volume       = {85},
 number       = {2},
 doi          = {10.1007/s10472-018-9597-7},
 url          = {http://doi.org/10.1007/s10472-018-9597-7},
)
@book(seventeen-provers,
 author       = {Freek Wiedijk},
 year         = {2006},
 title        = {The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence)},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/s11225-007-9093-2},
)