Happy Thanksgiving! Please note that there are no classes November 25th-December 1st.

MIT PRIMES/Art of Problem Solving

CROWDMATH 2018: Neural Codes

G
Topic
First Poster
Last Poster
crowdmath 2019 project on formalization
JGeneson   4
N Jul 18, 2019 by isar
Hello CrowdMath participants,

I would like your opinion about one of the projects for CrowdMath 2019.

Anthony Bordg has proposed a CrowdMath project on formalization using the Isabelle proof assistant. The purpose of the project will be to learn how to use Isabelle and to convert some math proofs so that Isabelle can verify them.

We would like to know what math proofs you are interested to formalize with Isabelle. One possibility is the first CrowdMath paper (which was published this year in EJOC: http://www.combinatorics.org/ojs/index.php/eljc/article/view/v25i1p5).

Are there other papers or proofs that you would be interested to formalize with Isabelle?
Please post any ideas here. For more information, see Anthony's original post below:

[quote=isar]Hi,

my name is Anthony Bordg, I'm a postdoc researcher at the University of Cambridge (UK). I would like to suggest an idea for a new CrowdMath project in 2019. This project will use the Isabelle proof assistant developed at Cambridge to formalize some fun mathematics. You can have a look at the Isabelle https://isabelle.in.tum.de/ webpage for further information.
What I have in mind is something similar to a previous collaborative project involving undergraduate students in Germany mentored by a few researchers. They formalized the so-called DPRM theorem using Isabelle, and their work resulted in the following publication https://easychair.org/publications/preprint/GhvC.
The formalization of mathematics has made nice progress over the last few decades, and now a substantial chunk of the undergraduate math curriculum has been formalized (see https://isabelle.in.tum.de/dist/library/HOL/index.html and https://www.isa-afp.org/). We might soon have a complete formalization of the Mathematical Tripos.
Be aware that formalized mathematical proofs should not be mistaken for automated proofs. The Isabelle proof assistant only checks that man-made proofs written with it are correct. Hence, writing mathematics with a proof assistant remains a highly creative endeavor.
I will try to remove as many barriers to participation as possible for those of you eager to take part in that project. We have tutorials and manuals for Isabelle, and there is a mailing list where anyone can ask for help. Moreover, I will be available on this forum to answer questions, and I will provide exercises to get started. Isabelle is very easy to install, easy to use, and it comes with a very nice level of automation. We should use GitHub https://github.com/ to share code.
At this stage I'm open to ideas of formalizations, so please let me know your favorite theorem/theory you would like to formalize. Jesse Geneson suggested that we could formalize the CrowMath paper published this year called Bounds on Parameters of Minimally Nonlinear Patterns http://www.combinatorics.org/ojs/index.php/eljc/article/view/v25i1p5 . This is certainly a nice possibility. The selected project will depend on its feasibility, the background available in the core Isabelle/HOL library and in the Archive of Formal Proofs, and its interest and originality.[/quote]
4 replies
JGeneson
Nov 25, 2018
isar
Jul 18, 2019
No more topics!
a