Email Gateway (Aug 19 2022 at 16:22): Email Gateway (Aug 19 2022 at 16:22):From: Dominic Mulligan <dominic.p.mulligan@googlemail.com>
Dear all,
Please forgive the slightly off-topic post.
The Foundations of Mathematics (FOM) [1] mailing list is a moderated forum
for mathematicians, computer scientists and philosophers with a (usually
professional) interest in foundational issues in mathematics and logic to
discuss and debate various topics, often in a lively and robust manner.
Recently, the idea of formal proof and the use of proof assistants in
mathematics seems to have caught the attention of the mathematicians on the
mailing list. This month alone [2] there have been three threads dedicated
to discussing various issues relating to formal proof, the use of proof
assistants in mainstream mathematics, how hard formal verification is for
those not well versed in the use of a proof assistant, the Flyspeck
project, and so on, and the topic has regularly come up in the past, albeit
intermittently (see e.g. [3] from two months ago).
Perhaps those with deep knowledge of proof assistants and their use, many
of which can be found on this list, but not yet aware of the FOM list,
would like to join in the discussion and answer some of the questions and
challenges being posed.
Thanks,
Dominic
[1]: http://www.cs.nyu.edu/mailman/listinfo/fom
[2]: http://www.cs.nyu.edu/pipermail/fom/2014-October/thread.html
[3]: http://www.cs.nyu.edu/pipermail/fom/2014-August/018057.html
Last updated: Apr 20 2024 at 04:19 UTC