*To*: Max Haslbeck <haslbema at in.tum.de>*Subject*: Re: [isabelle] International Olympiad in Isabelle?*From*: José Manuel Rodriguez Caballero <josephcmac at gmail.com>*Date*: Mon, 18 Jun 2018 16:07:25 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CANQq8HWb9VpYZu4QfRpYAWFcbACXUVP_qVThjOHTyf=jaU8oAQ@mail.gmail.com>*References*: <CAA8xVUgsMwhooWwmz8G-3_zaSiE-7k_JRisB14NfZGU0zeU39Q@mail.gmail.com> <CANQq8HWb9VpYZu4QfRpYAWFcbACXUVP_qVThjOHTyf=jaU8oAQ@mail.gmail.com>

> > max said: > The technical details aside, I think, the hardest part is to find suitable > tasks (mathematical theorems, riddles, programs + their verification, ...) > that are solvable within - say - 5 hours. One source of suitable mathematical tasks could be the problems-solutions section in American Mathematical Monthly (many great mathematician, including Paul Erdos and Jeffrey Lagarias, contributed with problems and/or solutions): https://www.maa.org/press/periodicals/american-mathematical-monthly Also, a good source of elementary mathematics is The Mathematical Gazzette (Cambridge): https://www.cambridge.org/core/journals/mathematical-gazette There is a lot of good elementary mathematics in the collected works of Pierre de Fermat, Leonhard Euler, James Joseph Sylvester, S. Ramanujan, Paul Erdos, etc. Finally, my preferred source of non-trivial elementary mathematics: the Jakob Perelman's books (Algebra can be Fun, Arithmetic for entertainment, Geometry for Entertainment, Mathematics can be Fun, etc.). I think that such a "proving contest" should be for highschool students, because at that age, they have a lot of free time to become wizards in some specific proof assistant. I remember that, when I was a teenager, I learned Pascal in high school just to participate in a national contest: that kind engagement changes teenager lives for good. José M. 2018-06-18 14:19 GMT+02:00 Max Haslbeck <haslbema at in.tum.de>: > Dear José, > > we had a similar idea for a "proving contest", implemented a prototype > version > and tested it with the Isabelle group here in Munich. > Simon and I wrote up a few pages documenting the idea: > http://www21.in.tum.de/~haslbema/documents/provingcontests_draft18.pdf > > We are planning to push this further in future. > The technical details aside, I think, the hardest part is to find suitable > tasks (mathematical theorems, riddles, programs + their verification, ...) > that are solvable within - say - 5 hours. > > cheers, > max > > > 2018-06-17 16:04 GMT+02:00 José Manuel Rodriguez Caballero < > josephcmac at gmail.com>: > >> Hello, >> I just want to suggest, as an abstract possibility, that in order to >> introduce proof-assistants in popular culture, to organize an >> International >> Olympiad in Isabelle could be a good strategy. I imagine such an Olympiad >> as many high school students in a room, in front of their computers, >> trying >> to mechanize the proof of a hard theorem from elementary mathematics that >> is written on a blackboard, e.g., a theorem due to Erdos or Ramanujan. To >> use papers to write the arguments is forbidden: the proof should go from >> their brain to Isabelle in a direct way. The first student who finishes >> the >> proof win (this can be checked in an automatic). >> >> Kind Regards, >> José M. >> > >

**References**:**[isabelle] International Olympiad in Isabelle?***From:*José Manuel Rodriguez Caballero

**Re: [isabelle] International Olympiad in Isabelle?***From:*Max Haslbeck

- Previous by Date: [isabelle] Isabelle2018-RC0: missing documentation for ISABELLE_TOOL_JAVA_OPTIONS
- Next by Date: [isabelle] the height of a Dyck path codified by balanced parentheses
- Previous by Thread: Re: [isabelle] International Olympiad in Isabelle?
- Next by Thread: Re: [isabelle] International Olympiad in Isabelle?
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list