Hi Stan, If I were to formalize this in Metamath, I'd use the first proof, but in a more calculational format.
I've attached it, unfortunately as a picture. Yes, this is a longer proof, but it seems somehow easier to me. Hope this helps someone... :-) [image: image.png] Groetjes, <>< Marnix Op do 27 feb. 2020 om 18:08 schreef 'Stanislas Polu' via Metamath < [email protected]>: > Hi all, > > I'm quite a beginner with Metamath (I have read a bunch of proofs, most of > the metamath book, I have implemented my own verifier, but I haven't > constructed any original proof yet) and I am looking to formalize the > following proof: > > IMO B2 1972: http://www.cs.ru.nl/~freek/demos/exercise/exercise.pdf > Alternative version: > http://www.cs.ru.nl/~freek/demos/exercise/exercise2.pdf > > (More broadly, I think this would be an interesting formalization to have > in set.mm given this old but nonetheless interesting page: > http://www.cs.ru.nl/~freek/demos/index.html) > > I am reaching out to the community to get direction on how should I go > about creating an efficient curriculum for myself in order to achieve that > goal? Any other advice is obviously welcome! > > Thank you! > > -stan > > -- > 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/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/78223c8d-eddf-4f84-970d-6b0cbb20dab9%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- Marnix Klooster [email protected] -- 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/CAF7V2P-2gAJsLSmnz-AtneyXNOGmG5w%3Dcn2gYVXk94FUQ5XdPg%40mail.gmail.com.
