I think this is holding Euclid's work to a higher standard that didn't exist at that time. I believe you're referring to "Proof-checking Euclid"(2019)[0], in wh

I think this is holding Euclid's work to a higher standard that didn't exist at that time. I believe you're referring to "Proof-checking Euclid"(2019)[0], in which the authors used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. Euclid Book I was written 2,300 years ago. I think it's reasonable that some "additional" axioms were occasionally implied. As [0] states, "[that] gap is filled by adding a 'circle–circle' axiom, according to which if circle C has a point inside circle K, and also a point outside circle K, then there is a point lying on both C and K." I'm not sure, but I feel like that might be reasonable to do for a reader of Euclid Book I in 300 B.C. So is the proof "invalid"? Yeah maybe, according to modern definitions. But I don't think the logic of that part of the proof was actually flawed, just under-presented. 0: https://link.springer.com/content/pdf/10.1007/s10472-018-9606-x.pdf https://link.springer.com/content/pdf/10.1007/s10472-018-960...