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.
