  Motivated by the recent 10 million dollar AIMO challenge, this paper targets
the problem of finding all functions conforming to a given specification. This
is a popular problem at mathematical competitions and it brings about a number
of challenges, primarily, synthesizing the possible solutions and proving that
no other solutions exist. Often, there are infinitely many solutions and then
the set of solutions has to be captured symbolically. We propose an approach to
solving this problem and evaluate it on a set of problems that appeared in
mathematical competitions and olympics.
