Subscribe to Events
From solving formal systems to building theories (and back)
Gabriel Poesia
Location: Hill 705
Date & time: Wednesday, 01 April 2026 at 10:00AM - 11:00AM
A famous essay by Gowers, “The two cultures of mathematics”, highlights a contrast between two attitudes towards mathematics: the problem-solving view where the point of “understanding” is to improve one’s ability to tackle problems, and the theory-building angle that sees the point of solving problems as improving one’s understanding (and mathematical theories). AI, for mathematics and arguably most domains, largely focuses on problem-solving given an existing background theory, but building theories themselves is comparably underexplored. This talk will consider what theory building can look like in two AI systems. First, we will consider the problem of tactic induction: given a set of formal proofs, find high-level tactics that simplify them, as measured by a compression objective. We’ll consider both a case study on learning tactics from educational algebra problems from Khan Academy, as well as tactics in the Rocq theorem prover. Learned tactics reveal domain-specific patterns in solutions and we show that they can help LLM-based provers. Then, we will describe ongoing work on Formal Disco, an open-ended system where complete new verified programs, from ideation to specification, implementation and proofs, are synthesized by LLM agents. Using open models over 10 days, our system generated the largest dataset of verified programs in the Dafny language to date, and we show how the data is useful to improve models at verification-relevant tasks, such as annotating methods with assertions and loops invariants. Although the evaluations of both systems will focus on pragmatic tasks, we will speculate further on implications of more powerful automated theory building systems.