人工智能、形式化方法与数学推理（AIMing）

“人工智能、形式化方法与数学推理”（AIMing）项目致力于支持创新计算与人工智能技术同数学推理新策略、新技术交叉领域的研究，目标是实现知识发现的自动化。数学推理是人类智能的一项核心能力，在知识发现中发挥着重要作用。过去几十年间，数学界和计算机科学界共同推动了机器辅助数学推理的研究，涵盖猜想、证明和验证等环节。这些工作既包括形式化方法和交互式定理证明器，也涉及人工智能技术的应用。近年来，随着技术的进步，数学科学、形式化方法和人工智能等领域对机器辅助数学推理的兴趣显著升温。反过来，这一领域的突破也有望对人工智能研究本身产生重要影响。