Some IMO problem solutions formalized in Isabelle/HOL

Stream: IMO-grand-challenge

[Filip Marić]

Hi, as part of their course on interactive theorem proving my students and I are working on formalizing IMO problems and solutions in Isabelle/HOL. It's not Lean, but I guess it might be interesting for people in this discussion forum. Our current work is available (https://github.com/filipmaric/IMO) and I hope that this repository grows over time (as students do their coursework). All files are written fully manually and I suppose that many steps in those proofs could be better automated - automating larger and larger parts of the proof might be a useful step towards your grand challenge.

[Johan Commelin]

Hi, welcome! (I think that part of the "challenge" is that other provers can also make an attempt :wink:)

[Kevin Buzzard]

How are you formalising geometry problems? Synthetically or with coordinates?

[Filip Marić]

Currently we skipped all geometry problems, as we were not aware of any synthetic geometry development that would suite our needs. Recently I have found out that there is a formalization of Tarski's geometry in Isabelle/HOL (ported from GeoCoq), so we might consider doing also some (synthetic) geometry.

[Daniel Selsam]

@Filip Marić Welcome and thanks for sharing!