A famous essay by Gowers, “T he two cultures of mathematics”, highlights a contrast between two attitude s towards mathematics: the problem-solving view where the point of “underst anding” 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 arguab ly most domains, largely focuses on problem-solving given an existing backg round theory, but building theories themselves is comparably underexplored. This talk will consider what theory building can look like in two AI syste ms. First, we will consider the problem of tactic induction: giv en a set of formal proofs, find high-level tactics that simplify them, as m easured by a compression objective. We’ll consider both a case study on lea rning tactics from educational algebra problems from Khan Academy, as well as tactics in the Rocq theorem prover. Learned tactics reveal domain-specific p atterns 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, implementa tion and proofs, are synthesized by LLM agents. Using open models over 10 d ays, our system generated the largest dataset of verified programs in the D afny language to date, and we show how the data is useful to improve models at verification-relevant tasks, such as annotating methods with asser tions and loops invariants. Although the evaluations of both systems w ill focus on pragmatic tasks, we will speculate further on implication s of more powerful automated theory building systems.