Proof-checking Euclid

Beeson, M; Narboux, J; Wiedijk, F

Wiedijk, F (reprint author), Radboud Univ Nijmegen, Inst Comp & Informat Sci, Toernooiveld 212, NL-6525 EC Nijmegen, Netherlands.

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2019; 85 (2-4): 213

Abstract

We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possi......

Full Text Link