Hi Marnix! Thanks for sharing. The proof I formalized[0] is very closed but I agree is also a bit more complicated.
Out of curiosity, where did you find that proof which has a very "formal" presentation? Best, -stan [0] http://us.metamath.org/mpeuni/imo72b2.html On Mon, Mar 23, 2020 at 6:38 PM Marnix Klooster <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAF7V2P-2gAJsLSmnz-AtneyXNOGmG5w%3Dcn2gYVXk94FUQ5XdPg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CACZd_0x56Ck-geksHLs0pRZwCLb_oaisqxyFpH4Ds5haXkrU9Q%40mail.gmail.com.
