> I'm hoping to contribute to the Elementary Geometry section, so I've been walking through > the current set.mm work due mostly to Thierry Arnoux, Mario Carneiro, and Scott Fenton. > This involves reading Schwabauser, something of a trick since it's in German and > I can't read German. (Hello Google translate!)
Very clearly I propose that we reactivate what I had done on the geometry of Euclid using Wayne Aitken's handouts. It's in English. It's very easily formalizable. All the preliminary definitions have already been entered. There's very rich material with Euclidean and non-Euclidean geometry. We can put that in the history section. And we can go on to formalize Euclid itself. And we can add links to Oliver Byrne's work because his proofs are very easy to understand and can help to understand the formalized version if we take care to stay close to the text. https://www.c82.net/euclid/ It won't compete with Schwabauser's version. The latter will be the official geometry in the main section. And the Euclid/Aitken version will be in a historical section. We will thus have a section that will follow the rules of the historical sections in that its purpose will be to be as close to Euclid as possible in order to be an aid to reading the Elements. And moreover David will not have to break his head to decipher a German text. Finally, being able to compare Schwabauser's and Euclid's versions will enrich both versions. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f9be1538-bc63-4f40-99fa-098a0e7f4957o%40googlegroups.com.
