Gabriel Poesia

AI has made quite remarkable progress in general game playing in the last decade, with AlphaZero being a prime example. Given a proper game -- a definition of possible states, a finite set of valid moves, and a notion of rewards --, modern deep reinforcement learning can master a range of games without requiring human data. This base methodology has been adapted to rather nonstandard games, such as protein folding and finding matrix multiplication algorithms. One of the most important "games" that humans play is mathematics. Math feels like a game in several ways, including that many people have fun with it, and that the rules are in principle well-defined. One of my main research questions is: how can we train agents to play the game of mathematics, in a general fashion, without relying on human-written proofs? Interactive theorem provers, like Lean, Coq and Isabelle, get very close to properly defining a general game of mathematics. In any of them, we can state arbitrary definitions,

AI has made quite remarkable progress in general game playing in the last decade, with AlphaZero being a prime example. Given a proper game -- a definition of possible states, a finite set of valid moves, and a notion of rewards --, modern deep reinforcement learning can master a range of games without requiring human data. This base methodology has been adapted to rather nonstandard games, such as protein folding and finding matrix multiplication algorithms. One of the most important "games" that humans play is mathematics. Math feels like a game in several ways, including that many people ha