Hi David, great work. I really like this presentation, because it is very precise, specific and complete, and it gives an illustrative impression of Metamath and mmj2.
I have only one remark: * Slides 1 and 2: You do not "prove a geometric proof" - you either "formalize a geometric proof" or "formally prove a specific geometry theorem". The rest seems to be perfect (I have to admit, however, that I did not go through slides 13-30 in detail...). Regards, Alexander On Wednesday, July 15, 2020 at 3:06:08 AM UTC+2, David A. Wheeler wrote: > > I'd love to hear comments on my draft presentation > "Proving Geometric Proof Schwabhäuser 4.6 in Metamath Proof Explorer": > > https://dwheeler.com/misc/Schwabhauser4.6.pptx > > This presentation focuses on Schwabhäuser theorem (“Satz”) 4.6 > as formalized by Thierry Arnoux in MPE theorem tgbtwnxfr ; it shows how > to recreate this proof using mmj2. My thanks to Thierry for his hard work! > > I'd be especially interested in tips that would reduce what > you'd need to know or guess to create this proof beyond what's already > stated in Schwabhäuser. > > --- David A. Wheeler > -- 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/d1d02c28-4dce-49f6-8f5b-80bfd9d0fcc5o%40googlegroups.com.
