solving procedure

Stream: IMO-grand-challenge

[Miroslav Olšák]

Hello everyone,
I am thinking about how ITPs are suited for mathematical problem solving. There are three levels of language complexity for mathematics. First, you just need to write down the problem statement, second, you want to write down a solution (that is what ITPs are usually used for), and third, you want to capture the thoughts during the problem solving process. That requires tools for problem exploration, and also sometimes not so rigid reasoning. The question is, how well is Lean suitable for that? Do you think that you could solve an IMO problem inside Lean (without using paper) in a better way than writing most of your thoughts into the comments? As an experimental IMO domain for that, I propose (non-geometrical) Combinatorics. It is often algorithmical, therefore relativelly suited for computers, and it also often offers good room for exploration. As an example what I mean by the problem solving process, I tried to capture my thoughts during solving of the C5 problem from 2009 Shortlist: http://www.olsak.net/mirek/human-imo-solving/2009-C5 (to be honest, I cheated a bit because I originally thought I solved it when I did not, but as a demonstration it should serve well).
I can try to solve more problems in this way to provide more examples, if you are interested.

[Miroslav Olšák]

By the way, I am currently also working on a standalone application for geometrical problems supporting some sort of trivial logic, also with the intention to be also usable as a problem solving tool: https://github.com/mirefek/geo_logic

[Miroslav Olšák]

A few more examples of my thought processes: http://www.olsak.net/mirek/human-imo-solving.php Solving IMO problems is actually quite fun :-). The question is to what extent such problem-solving processes could be formalized.