Computer environments for math problem solving

Although the interactive theorem provers managed to capture reasonably well the language of proofs, they are still behind in following the problem-solving process, especially in less algebraic domains of mathematics. We study this issue by looking at specific cases of problems, and trying to find a reasonably close computer approximation of what a mathematician playing with the problem does. In this talk, a particular focus will be given to the grasshopper problem -- IMO-2009-6.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180