Re: [isabelle] International Olympiad in Isabelle?



>
> 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.
>>
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.