Symbolic Computation for All the Fun

TL;DR

This work tackles the problem of finding all functions $f:\mathbb{R}\to\mathbb{R}$ that satisfy a given specification, a task central to mathematical competitions and the $10$-million AIMO challenge. It introduces a template-and-quantifier-elimination framework that leverages SMT solvers (e.g., $\text{cvc5}$, $\text{Z3}$) and Waldmeister, together with QE, to derive and verify the full solution class within fixed functional templates. The authors apply the method to a corpus of problems transcribed into SMT2 (87 problems) and demonstrate automated template verification, QE-based extraction of solved forms, and hand-solution verification, including cases where the solution set is a simple, unique function. The results illustrate that symbolic computation can yield complete solution descriptions for nontrivial functional equations in competition-style settings, guiding future integration with additional synthesis techniques and more expressive templates.

Abstract

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.