IneqAgent：结合符号计算的 Lean Agent 不等式证明
英文标题：IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
IneqAgent 是一个结合大语言模型推理与符号计算的 Agent 框架，面向 Lean 中的不等式证明。原文指出，形式化不等式证明需要数学推理和精确计算，并经常通过中间引理及目标重述将二者连接起来。所提供的摘要在框架介绍处截断，未包含实验数据、性能结论或对开发者的具体意义。
打开原文相关 4.8 · 机会 0
2.1 KB
612 B
380 B
9.1 KB
32.7 KB
22.8 KB
24.2 KB
34.7 KB
中文
形式化不等式证明需要数学推理和精确计算，二者通常通过中间引理及目标重述连接起来。本文介绍 IneqAgent，这是一个结合大语言模型推理与符号计算的 Agent 框架……
注：所提供的原文摘要在此处截断。
BibTeX 格式引用
所提供的原文未包含 BibTeX 引用内容。
English / 原文
BibTeX formatted citation
×