Peano: Learning Formal Mathematical Reasoning Without Human Data

11/08/2023 2:00 pm - 3:00 pm
Michael Douglas
CMSA Room G10
Address: CMSA, 20 Garden Street, Cambridge, MA 02138 USA

New Technologies in Mathematics Seminar

Speaker: Gabriel Poesia, Dept. of Computer Science, Stanford University

Title: Peano: Learning Formal Mathematical Reasoning Without Human Data

Abstract: Peano is a theorem proving environment in which a computational agent can start tabula rasa in a new domain, learn to solve problems through curiosity-driven exploration, and create its own higher level actions. Gabriel will describe the system, present case studies on learning to solve simple algebra problems from the Khan Academy platform, and describe work on progress on learning the Natural Number Game, a popular introduction to theorem proving in Lean for mathematicians.