无需人类演示的奥林匹克代数不等式证明

解决奥林匹克水平的数学问题是机器智能和自动推理的重要进展。然而，当前的机器学习方法在无法解决奥林匹克水平的问题，特别是欧几里得平面几何问题，由于缺乏大规模高质量数据集。代数系统的挑战更为严峻，这些系统在有限条件下包含无限的推理空间。为此，我们提出 AIPS，即一种代数不等式证明系统，能够自主生成复杂的不等式定理，并在不要求人类演示的情况下有效解决奥林匹克水平的不等式问题。在混合推理中进行证明搜索时，实施了一种针对生成数据集的值课程学习策略，以提高证明性能，展现出强大的数学直觉。在 20 个国际数学奥林匹克水平不等式问题的测试集上，AIPS 成功解决了 10 个问题，超越了最先进的方法。此外，AIPS 在没有人工干预的情况下自动生成了大量非平凡的定理，其中一些已被专业选手评估，被认为达到了国际数学奥林匹克水平。值得注意的是，其中一个定理被选为 2024 年某大城市数学奥林匹克的 competition 问题。