[isabelle] The goals of Xena Project (was: International Olympiad in Isabelle?)



>
> max wrote [about the International Olympiad in Isabelle]:
> 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.


Last Friday I solved a mathematical problem from the Putnam Mathematical
Competition and immediately after I formally verified my solution in
Isabelle/HOL. It was nearly 5 hours of work (including solution and formal
verification). I stopped for a coffee and food. So, I think that an
International Olympiad in Isabelle will be possible in such conditions.

The problem was ARITHMETIC PROGRESSIONS in the following link:
https://www.ocf.berkeley.edu/~wwu/riddles/putnam.shtml

My solution is here (it is not the most elegant formalization, because I
was in a hurry trying to be as fast as possible):
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/blob/master/ArithProgRelPrimes.thy

After the formal verification, my understanding of the problem was much
better than before.

I hope that one day the goals of the so-called Xena Project, i.e.,
mathematical education with proof assistants, will be a current reality in
most of universities of the world:
https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/

Competition is the best way to motivate people to do something new.

Kind Regards,
José M.

El lun., 18 jun. 2018 a las 8:19, Max Haslbeck (<haslbema at in.tum.de>)
escribió:

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