SMT and Functional Equation Solving over the Reals: Challenges from the IMO

2025/04/22 by Chad E. Brown, Karel Chvalovský, Brown, Chad E. +7 · 1 voice · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.2504.15645

arxiv published 2025/04/22 · arxiv updated 2025/07/09

Abstract

We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical Olympiad (IMO), where the task is to determine all solutions to constraints on an uninterpreted function. Although these problems require only high-school-level mathematics, state-of-the-art SMT solvers often struggle with them. We propose several techniques to improve SMT performance in this setting.

Citations

• Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad
• MathConstruct: Challenging LLM Reasoning with Constructive Proofs
• Symbolic Computation for All the Fun
• Deciding Predicate Logical Theories of Real-Valued Functions
• Fair and Adventurous Enumeration of Quantifier Instantiations
• Simplify: a theorem prover for program checking
• Real quantifier elimination is doubly exponential

Cited by

• From MBQI to Enumerative Instantiation and Back

Discussions

• In our recent CADE paper we looked at how SMT solvers can contribute to the solving of functional equations, which often appear in math olympiads and competitions arxiv.org/pdf/2504.15645 #SMT #IMO #A [bsky, 0 points, 0 comments]

Related

• Leveraging linear and mixed integer programming for SMT
• SMT-Solving for the First-Order Theory of the Reals
• Satisfiability Modulo ODEs
• Satisfiability Modulo Exponential Integer Arithmetic
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers