I love how you lot just redefine words to suit your purpose:
https://www.etymonline.com/word/formal
"late 14c., "pertaining to form or arrangement;" also, in philosophy and theology, "pertaining to the form or essence of a thing," from Old French formal, formel "formal, constituent" (13c.) and directly from Latin formalis, from forma "a form, figure, shape" (see form (n.)). From early 15c. as "in due or proper form, according to recognized form," As a noun, c. 1600 (plural) "things that are formal;" as a short way to say formal dance, recorded by 1906 among U.S. college students."
There's not a much better description of what Euclid was doing.
What you mean is someone has redefined the word to suit their purpose, which is precisely what I pointed out at the top.
Edit to add: this comment had a sibling, that was suggesting that given a specific proof assistant requires all input to be formal logic perhaps the word formal could be redefined to mean that which is accepted by the proof assistant. Sadly this fine example of my point has been deleted.
Every mathematician understands what a formal proof is. Ditto a formal statement of a mathematical or logical proposition. The mathematicians of 100 years ago also all understood, and the meaning hasn't changed over the 100 years.
> The mathematicians of 100 years ago also all understood, and the meaning hasn't changed over the 100 years.
Isn't that the subject of the whole argument? That mathematicians have taken the road off in a very specific direction, and everyone disagreeing is ejected from the field, rather like occurred more recently in theoretical physics with string theory.
Prior to that time quite clearly you had formal proofs which do not meet the symbolic abstraction requirements that pure mathematicians apparently believe are axiomatic to their field today, even if they attempt to pretend otherwise, as argued over the case of Euclid elsewhere. If the Pythagoreans were reincarnated, as they probably expected, they would no doubt be dismissed as crackpots by these same people.
Not all proofs are formal, and most published papers are not formal in the strictest sense. That is why they talk about "formalizing" a proof if there is some question about it. It is that formalization process which often finds flaws.
https://www.etymonline.com/word/formal "late 14c., "pertaining to form or arrangement;" also, in philosophy and theology, "pertaining to the form or essence of a thing," from Old French formal, formel "formal, constituent" (13c.) and directly from Latin formalis, from forma "a form, figure, shape" (see form (n.)). From early 15c. as "in due or proper form, according to recognized form," As a noun, c. 1600 (plural) "things that are formal;" as a short way to say formal dance, recorded by 1906 among U.S. college students."
There's not a much better description of what Euclid was doing.