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/E1jvVs6-000517-SP%40rmmprod06.runbox.
