Euclids rigor was remarkable for 300 BC, but its not really what we think of as rigorous now. Even the first theorm has several fairly obvious flaws (as the li

Euclids rigor was remarkable for 300 BC, but its not really what we think of as rigorous now. Even the first theorm has several fairly obvious flaws (as the linked commentary points out). So you probably wouldn't have much Euclid left if you tried to make a machine checked version of Euclid. Many people post-300BC have done more rigorous treatments of plane geometry. Most famously Hilbert, who had (IIRC) 21 axioms.