Imagine an AI that could crack the toughest math problems, like those faced by Olympiad competitors. That's the ambitious goal explored in new research on automating the proof process for functional equations, a notoriously challenging area of mathematics. Functional equations involve puzzles where the goal is to find unknown functions that satisfy specific conditions—think of it as algebra on steroids. The challenge lies in the massive search space of possible proof steps, making it computationally expensive for traditional automated theorem provers (ATPs). This new research introduces the Functional Equation Automated Solver (FEAS), an AI agent that uses a clever approach. Instead of brute-force searching through all possible steps, FEAS guides a Large Language Model (LLM) to first develop a high-level proof strategy in plain English. Then, the LLM translates this strategy into the formal language of the Lean theorem prover. This “think first, then write” approach mimics how human mathematicians approach proofs, generating a structured and strategically sound solution. To make it even more efficient, FEAS incorporates special mathematical tricks, or heuristics, into the LLM’s prompting, guiding it toward promising avenues. Tested on a custom dataset of functional equation problems ranging from simple to Olympiad-level difficulty, FEAS shows promising results, outperforming existing methods, especially on simpler problems. However, the most challenging problems still pose a significant hurdle. The research highlights two key problems: figuring out the right mathematical steps and translating those steps into the precise, formal language a computer understands. While AI isn't ready to replace Olympiad mathematicians just yet, this research provides a glimpse into a future where AI plays an integral role in unraveling complex mathematical puzzles and potentially discovering new mathematical knowledge.