Peano

Stream: Machine Learning for Theorem Proving

[Jason Rute]

Cross posting this here:

Junyan Xu said:

CMSA New Technologies in Mathematics seminar today at 2 PM -- Gabriel Poesia

Gabriel Poesia of the Stanford CS dept. will speak today at 2 (EST) on  

``Peano: Learning Formal Mathematical Reasoning Without Human Data’'

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.

(removed Zoom link as the talk ended, will post a Youtube link when it's up)

The paper https://arxiv.org/abs/2211.15864 has been there last year, but there's new progress apparently.

[Junyan Xu]

Hmm I just checked and the recording was apparently there 10 hours ago :tada: