Designing Game of Theorems
This work addresses theorem proving, a foundational challenge in automated reasoning and AI, by introducing a novel competitive framework, though it appears incremental as it builds on existing ideas from game-based AI.
The paper tackles the problem of improving theorem provers by analyzing similarities and differences between theorem proving and the game of Go, and proposes a competitive system where provers evolve to prove user-provided conjectures.
"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.