Hi David, This looks very good!
It's nice to have a step-by-step explanation of how the proof is built. I think you got it right. A few remarks: Maybe I would rephrase the text in slide 12: It's true you need to prove that x exists, but actually at the point in time you use the theorem you already have ` E. x e. A ` as a hypothesis, so I would rather write /Set variable //x is a point you know exists, and you need to use in the construction./ You could see it as an intermediate construction point. It shall not appear in the result ` ch `.// Also maybe slide 4, ` .~ ` shall be named a "relation" rather than an "operator" (` I ` and ` .- ` are indeed operators, they return classes). Slide 4, you have too many parentheses in ( ph -> ( B e. P ) ), you don't need them around B e. P! Slide 7, /To convert “XX=YY” into “XX e. (AA I BB)”/, I'm not sure why you double the letters here. You could maybe write "to transfer the membership between X and Y which are known to be equal"? I think slide 7 gives a very good overview of the proof, the rest is mainly glue around it :-) It's very nice that you went through all the steps, this could serve as a good introduction. BR, _ Thierry On 15/07/2020 09:06, 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/d5127b10-23f5-7a92-7565-512e233f8f30%40gmx.net.
