Very nice. Seems definitely beneficial to prepare a proof for formalization.
-stan On Tue, Mar 24, 2020 at 9:00 AM Marnix Klooster <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAF7V2P8PEpV8dy-dkmcVaUo9CAZAi1iMw41%2BXsa-K07Lyi2D7g%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_0xW7E6CcGbfJ9yY_vCNTegFO7PnaqYO5q25XQjktJ7mEA%40mail.gmail.com.
