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.