Acorn：革新性的AI定理证明器

本文介绍了Acorn，一款与传统交互式定理证明器（如Lean）截然不同的AI定理证明器。Acorn采用对话式交互方式，用户逐步提出断言，系统自动验证。这与人类证明过程更贴近，避免了繁琐的类型声明和预定义定理的查找。Acorn使用简单的ML模型，在证明过程中提供辅助，并指出需要用户干预的部分，提升了证明效率和可理解性。相比Lean等系统，Acorn更注重直观性和自然语言表达，展现了人机协作在数学证明领域的巨大潜力。