Hi Stan, I designed and wrote that proof myself. :-) This is the style designed and advocated by Edsger W. Dijkstra and this collaborators. See his EWD1300 <https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html> for an overview and his reasoning.
So what I like about this proof and this style, is several things, like avoiding rabbits-out-of-hats and instead trying to provide insight: "why would one think about taking a least upper bound here?"; preferring a direct style instead of resorting to contradiction; making explicit which assumptions are used where; making the proof easier on the reader so that they don't have to guess why a certain step is correct; and this style of proof is (at least for me) easier to reinvent later: just go through the same heuristics again and most of the proof writes itself. For example, the original proof starts with the rabbit 2k (so 2 sup |f(z)|) and then makes that expression more complex. The simple act of inverting the order of that calculation makes the proof easier to understand, at least for me, but I think for many other readers as well. And it makes proofs easier to formalize, I think. -Marnix Op ma 23 mrt. 2020 om 21:05 schreef 'Stanislas Polu' via Metamath < [email protected]>: > 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 > <https://groups.google.com/d/msgid/metamath/CACZd_0x56Ck-geksHLs0pRZwCLb_oaisqxyFpH4Ds5haXkrU9Q%40mail.gmail.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/CAF7V2P8PEpV8dy-dkmcVaUo9CAZAi1iMw41%2BXsa-K07Lyi2D7g%40mail.gmail.com.
