Filip Marić (Jun 09 2020 at 17:03):
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 (Jun 09 2020 at 17:04):
Hi, welcome! (I think that part of the "challenge" is that other provers can also make an attempt :wink:)
Kevin Buzzard (Jun 09 2020 at 17:09):
How are you formalising geometry problems? Synthetically or with coordinates?
Filip Marić (Jun 09 2020 at 17:12):
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 (Jun 09 2020 at 18:39):
@Filip Marić Welcome and thanks for sharing!
Last updated: Aug 05 2021 at 04:14 UTC