Email Gateway (Aug 22 2022 at 17:37): Email Gateway (Aug 22 2022 at 17:37):From: Makarius <makarius@sketis.net>
Incidentally something like this has happened a few weeks ago at the
national level (of Germany):
https://sketis.net/2018/jugend-forscht-hilbert-meets-isabelle
The Isabelle team even won a special prize by the Federal President of
Germany, Frank-Walter Steinmeier.
There will be a presentation about this (still ongoing) project at the
Isabelle Workshop 2018 at Oxford:
https://easychair.org/smart-program/FLoC2018/Isabelle-2018-07-13.html#talk:71275
Makarius
Email Gateway (Aug 22 2022 at 17:38):From: Max Haslbeck <haslbema@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
Email Gateway (Aug 22 2022 at 17:39):From: Makarius <makarius@sketis.net>
An interesting paper.
Note that "the ML level" no longer exists in Isabelle today. You mean
"Isabelle/ML", which is properly integrated into Isabelle/Isar for more
than 10 years. In the past, end-users were accustomed to the Poly/ML
bootstrap environment, which is still available in "isabelle process"
and "isabelle console" today, but rarely used directly in applications.
Moreover note that the brief discussion about the 'sorry' command vs.
checking oracle tags in thm values is unfounded. Neither the Isabelle
documentation nor the implementation supports that claim.
Concerning the general mental model of a bullet-proof checker that can
run unattended and cannot be abused: I don't believe that Isabelle can
ever deliver that. It was not constructed with that idea in mind: after
decades of following a model of benevolent users that don't shoot
themselves in the foot, it is infeasible to do differently in a posthoc
fashion. You need a different proof checker for that, but I don't know a
suitable system.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC