Watch a Harvard CMSA seminar presentation where Stanford University Computer Science researcher Gabriel Poesia introduces Peano, an innovative theorem proving environment designed for autonomous learning. Discover how computational agents can begin with no prior knowledge, develop problem-solving abilities through curiosity-driven exploration, and generate their own sophisticated reasoning strategies. Explore case studies demonstrating Peano's application to Khan Academy algebra problems and learn about ongoing research applying the system to the Natural Number Game, a popular introduction to formal theorem proving in the Lean programming language. Gain insights into how artificial intelligence can learn mathematical reasoning without relying on human training data.
Overview
Syllabus
Gabriel Poesia | Peano: Learning Formal Mathematical Reasoning Without Human Data
Taught by
Harvard CMSA
Related Courses
-
Frontier of Formal Theorem Proving with Large Language Models - DeepSeek-Prover Series
-
Machine Learning and Theorem Proving in Formal Languages
-
Bridging Informal and Formal Mathematical Reasoning with Neural Language Models
-
Solving Olympiad Geometry Without Human Demonstrations - AlphaGeometry's Automated Reasoning Approach
-
From Word Prediction to Complex Skills: Data Flywheels for Mathematical Reasoning
