Someone sent me a link to this year’s IMO questions this afternoon at work, and the first one caught my eye because it looked like a relatively straightforward functional equation question: find all 
Now formalisation is hard, so I knew I would end up getting bogged down in details and things which looked straightforward on paper would end up messy. At some point someone divides by 2, that looks a bit problematic with the integers, and then there’s some integer induction — I kept waiting to get to the place where it was all going to go horribly pear-shaped.
But that place never came. Powerful tactics like convert and ring , the conv mode, and a sensible induction procedure for the integers meant that the Lean proof flowed just as the paper proof had done. Here it is! That’s a link to the source code, which you can cut and paste into a local Lean project if you have Lean installed on your computer, or you can even inspect it online here if you can face the 30 second wait while a transient version of Lean installs itself on your computer in order to make it work. It probably took over half an hour, but under an hour, to finish the formalisation of that IMO question (i.e. time spent at the computer). Of course the question is not too hard — but that’s not the point.
The point is this. Before I got into the formalisation business, it was “obvious” to me that formalising questions like this should be easy. When I actually started, it became very clear to me very quickly that formalising IMO questions would be very hard, because formalising anything with content is hard. But the nice surprise is that actually, once one has a grip on formalisation, if one is working in an area which is “sufficiently close to the axioms” like elementary number theory or algebra, maybe nowadays in Lean it really is becoming as easy as I always “knew” it would be.
PS soon to appear on the wall at the Royal Academy of Art:
Xena 
Fantastic! We’re going to have to start running live Lean sessions post IMO. 🙂
LikeLiked by 2 people
I tried formalising some olympiad problems (problems 1 and 4 from the recent BMO2 paper) to see what that’s like in practice. Since I got Lean to accept complete proofs of both problems, formalising (some) algebra and number theory olympiad problems does indeed seem to be accessible to beginners with no formalisation experience at all beyond the natural number game and Lean maths challenges (at least if those beginners have a high tolerance for incomprehensible Lean error messages whenever they get something wrong). Though it was also very time-consuming (about a day per problem) and resulted in hundreds of lines of Lean code per problem, no doubt non-beginners would produce much shorter code, much quicker.
Both problems had places where I wanted to use some trivial lemma that I might have hoped would be in Lean’s standard library or mathlib but couldn’t find there (though I think some of those were actually a case of missing a more general result that was present). They also had places where I might have hoped for more automation to dispose of things that are obviously trivial to a human. For some reason it was the easier problem that got more bogged down in proving details of trivialities (modular arithmetic manipulations that didn’t seem to have a tactic that would just get rid of them all); in most of the problem 4 proof, the things that are mathematically trivial tended to match things that could be disposed of quickly with the field_simp, ring and linarith tactics.
LikeLike
Joseph that is really cool 😀 Are the proof scripts publically available?
LikeLike
Not public at present. Are such beginner formalisations of olympiad problems actually useful to someone (other than the person who did the formalisation in the first place, who learns things by making the formalisation attempt)? The places where it seemed there might be some more general trivial lemma (i.e. something of more general use) that I couldn’t find in mathlib mostly haven’t been refactored yet to state such intermediate results in general form, although I’ve done some cleanups after first doing the formalisations.
(I haven’t yet attempted to formalise BMO2 problem 3, although it might be a good exercise in seeing if I can figure out Lean’s interface for working with finite sets. As mathlib has no Euclidean geometry at present, it’s probably not ready to attempt even to state problem 2.)
LikeLike
Goofy maths like Olympiad questions all fits nicely into https://github.com/leanprover-community/mathlib/tree/master/archive
LikeLike
I certainly don’t think my beginner proofs are up to mathlib standards! I’ve now made those proofs available after a few more cleanups, with some of the trivial lemmas that feel more generally applicable factored out to separate files p1_lemmas.lean and p4_lemmas.lean. (I don’t yet have a clear feeling for where the division lies between trivial lemmas that belong in mathlib and trivial lemmas that don’t belong in mathlib and that users should prove themselves as needed by composing relevant mathlib lemmas.)
LikeLike