设计定理游戏
Designing Game of Theorems
摘要：
“定理证明类似于围棋。所以，我们可以使用深度学习来改进我们的证明器，就像DeepMind开发的超级计算机围棋程序AlphaGo一样。“这种乐观情绪在AITP 2017的参与者中得到了观察。但定理证明真的和围棋相似吗？在本文中，我们首先确定它们之间的相似性和差异，然后提出了一个系统，在该系统中，各种证明者不断相互竞争，不断改变自己，直到他们证明用户提供的证明。
英文摘要：
"Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such optimism has been observed among participants of AITP2017. But is theorem proving really similar to Go? In this paper, we first identify the similarities and differences between them and then propose a system in which various provers keep competing against each other and changing themselves until they prove conjectures provided by users.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
