One olympiad geometry problem formalised

Stream: IMO-grand-challenge

[Joseph Myers]

I've now completed formalising a solution to an easier-than-IMO olympiad geometry problem, so completing formalising one problem in each olympiad subject area (having formalised the other three problems on that paper some time ago). That geometry solution has about 1000 lines of Lean proving results that seem generically relevant for mathlib (parts are PRs #4088, #4116, #4127, #4128; other parts either depend on those PRs, or need reworking to be more general / cleaning up before PRing).

I expect many olympiad geometry problems can't yet be stated in a very clean way because relevant definitions aren't in mathlib. And there are definitely questions to resolve about the conventions for how to state such problems (and non-geometry problems that are started for human contestants in geometrical terms) for the IMO Grand Challenge, and if you want to do synthetic geometry solutions you'll still need to add lots more definitions and lemmas to support such solutions. But it's clearly "just" a matter of adding lots more definitions and lemmas to mathlib to make it possible to state all 362 past IMO problems (soon to be 368) and solutions to them. (And I tend to think that filling out mathlib in such areas should be just as much part of work on the IMO Grand Challenge as attempting to get AIs to prove things.)

[Daniel Selsam]

And I tend to think that filling out mathlib in such areas should be just as much part of work on the IMO Grand Challenge as attempting to get AIs to prove things.)

I agree. I am optimistic that ML will provide critical speedups in search down the road, but I do not expect it to be a panacea. Formalization is the driving force of the project: developing the definitions, lemmas, tactics, and strategies that transform an a priori hopeless search space into one that is merely intractable.