Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested proofs may look plausible, but cannot be trusted without rigorous checking. We present a framework, called LLM+CAS, and an associated tool, O-Forge, that couples frontier LLMs with a computer algebra systems (CAS) in an In-Context Symbolic Feedback loop to produce proofs that are both creative and symbolically verified. Our focus is on asymptotic inequalities, a topic that often involves difficult proofs and appropriate decomposition of the domain into the "right" subdomains. Many mathematicians, including Terry Tao, have suggested that using AI tools to find the right decompositions can be very useful for research-level asymptotic analysis. In this paper, we show that our framework LLM+CAS turns out to be remarkably effective at proposing such decompositions via a combination of a frontier LLM and a CAS. More precisely, we use an LLM to suggest domain decomposition, and a CAS (such as Mathematica) that provides a verification of each piece axiomatically. Using this loop, we answer a question posed by Terence Tao: whether LLMs coupled with a verifier can be used to help prove intricate asymptotic inequalities. More broadly, we show how AI can move beyond contest math towards research-level tools for professional mathematicians.

翻译：大型语言模型近期在解决国际数学奥林匹克竞赛和普特南数学竞赛问题上展现了卓越能力；然而其在研究数学领域的作用仍相当有限。关键难点在于验证：所提出的证明看似合理，但未经严格检验仍不可信。我们提出了一个名为LLM+CAS的框架及其配套工具O-Forge，该框架将前沿大型语言模型与计算机代数系统通过上下文符号反馈循环相结合，生成兼具创造性且经过符号验证的证明。我们的研究聚焦于渐近不等式——这一常涉及复杂证明且需将定义域恰当分解为“正确”子域的主题。包括陶哲轩在内的众多数学家曾指出，利用人工智能工具寻找合适的分解策略对研究级渐近分析极具价值。本文证明，LLM+CAS框架通过结合前沿大型语言模型与计算机代数系统，在提出此类分解方案方面表现出显著效能。具体而言，我们使用大型语言模型建议定义域分解方案，并借助计算机代数系统（如Mathematica）对每个子域片段进行公理化验证。通过该循环机制，我们回答了陶哲轩提出的问题：耦合验证器的大型语言模型能否用于证明复杂的渐近不等式。更广泛而言，本研究展示了人工智能如何超越竞赛数学范畴，发展为面向专业数学家的研究级工具。