# Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent

arXiv: https://arxiv.org/abs/2407.14521 · HTML: https://mlsanity.com/paper/2407.14521/

## Key facts

- No citing papers in the map yet (data through 7 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 13 of its 25 references that are in the map.
- First posted on arXiv 5 Jul 2024.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 13 of 13)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)

## Abstract (arXiv)

Automated Theorem Proving (ATP) faces challenges due to its complexity and computational demands. Recent work has explored using Large Language Models (LLMs) for ATP action selection, but these methods can be resource-intensive. This study introduces FEAS, an agent that enhances the COPRA in-context learning framework within Lean. FEAS refines prompt generation, response parsing, and incorporates domain-specific heuristics for functional equations. It introduces FunEq, a curated dataset of functional equation problems with varying difficulty. FEAS outperforms baselines on FunEq, particularly with the integration of domain-specific heuristics. The results demonstrate FEAS's effectiveness in generating and formalizing high-level proof strategies into Lean proofs, showcasing the potential of tailored approaches for specific ATP challenges.