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.

翻译：自动定理证明（ATP）因其复杂性与计算需求而面临挑战。近期研究探索了使用大语言模型（LLM）进行ATP动作选择，但这些方法可能消耗大量资源。本研究提出了FEAS，一个在Lean中增强COPRA上下文学习框架的智能体。FEAS优化了提示生成与响应解析，并针对函数方程融入了领域特定的启发式方法。同时，本研究引入了FunEq——一个包含不同难度函数方程问题的精选数据集。FEAS在FunEq上表现优于基线方法，尤其是在结合领域特定启发式方法时。结果表明，FEAS能有效生成高级证明策略并将其形式化为Lean证明，这彰显了针对特定ATP挑战定制化方法的潜力。