From Proof to Program: CMU and the Rise of AI-Driven Mathematics

From generating proofs to verifying complex theorems, new AI-driven tools are changing how mathematicians work, collaborate and even define knowledge itself. At Carnegie Mellon University, a group of researchers is helping lead that transformation by bringing together logic, machine learning and automated reasoning.

At the center of that effort is Jeremy Avigad, a professor in the Dietrich College of Humanities and Social Sciences’ Department of Philosophy and the Mellon College of Science’s Department of Mathematical Sciences, whose work in formalized mathematics is reshaping how proofs are written, checked and shared.

“This is an exciting time for mathematics, as new technologies offer opportunities for exploration and discovery,” Avigad said.

Carnegie Mellon’s strength lies not just in any one approach, but in the intersection of three: interactive theorem proving, neural AI and automated reasoning. Together, these areas form the foundation of a broader effort connected to the National Science Foundation-funded Institute for Computation and AI for Research in Mathematics (ICARM), which aims to advance AI methods for mathematical discovery and collaboration.

Building a New Mathematical Infrastructure

Avigad’s work focuses on formalization — the process of translating mathematical ideas into a precise, computer-verifiable language. At the heart of this effort is Lean, an open-source proof assistant that allows mathematicians to write proofs that a computer can check line by line. Alongside it is Mathlib, a rapidly growing, community-driven library of formally verified mathematics.

“Interactive proof assistants like Lean support the digitization of mathematics in much the same way that word processors support the digitization of natural language,” Avigad said.

Unlike traditional mathematical writing, which relies on human interpretation, formalized mathematics eliminates ambiguity, because every step must be explicitly justified.

“Formalization meets a high standard of rigor and precision, both of which are fundamental to mathematics,” Avigad said.

Formal verification can help ensure correctness in fields ranging from software engineering to cryptography. It also opens new possibilities for education, giving students tools to explore proofs interactively and receive immediate feedback.

At the same time, Avigad emphasizes that formal systems are not replacing mathematicians but augmenting their work.

“The goal is to provide mathematicians with new ways to do the things we want to do,” Avigad said.

Bridging Symbolic and Automated Reasoning 

While Lean and Mathlib provide a framework for verifying proofs, automated reasoning systems focus on finding them.

Marijn Heule, an associate professor in the School of Computer Science, focuses on solving hard-combinatorial problems in areas such as formal verification, number theory and extremal combinatorics.

“Automated reasoning is about getting computers to solve problems that require logical deduction, and to produce a proof that the answer is correct,” Heule said.

These systems, often built on techniques such as satisfiability (SAT) solving, have been used to tackle problems that would be difficult for humans alone. They play a critical role in formal verification, ensuring that systems behave as intended — from hardware design to large-scale computational processes. 

“These tools verify that the hardware and software we use every day behave correctly. They have also resolved long-standing open problems in mathematics, occasionally with gigantic proofs,” he said.

At Carnegie Mellon, automated reasoning builds on a long tradition of research in logic and verification. Heule’s work extends that legacy into new domains, including mathematics itself. While automated reasoning excels at exhaustive search and guaranteed correctness, it operates differently from interactive systems like Lean, which rely on human guidance.

“Interactive systems shine when a proof needs insight and structure. Automated systems shine when millions of cases must be checked without a single mistake,” Heule said. 

Together, these approaches are complementary: automated systems can explore vast spaces of possibilities, while interactive systems provide structure and verification.

Neural AI Enters the Equation

A third piece of the puzzle comes from neural AI — particularly large language models (LLM) that can generate mathematical text and even attempt proofs. 

Sean Welleck, an assistant professor in the Language Technologies Institute, studies how neural systems can learn structured reasoning.

“Neural AI models like LLMs are very flexible: they can be trained to write essays or to chat with you, but also to write mathematical proofs and solve complicated problems. We're seeing these AI methods intersect with the mathematics community more and more, so it's an exciting time,” Welleck said.

Unlike traditional automated reasoning, neural models learn patterns from data. This allows them to generate conjectures, suggest proof strategies and work in ways that resemble human intuition. By connecting neural models to proof assistants, researchers can combine AI with the certainty of formal verification.

“A key limitation of LLMs is that we don't know whether the math that they produce is correct or not. Lean gives a way to automatically verify that math produced by the AI is correct, making the two very synergistic,” Welleck said. 

A Shared Vision Through ICARM

These complementary approaches — formalization, automated reasoning and neural AI — converge in ICARM, an initiative designed to advance AI-driven mathematics.

The institute’s mission includes fostering collaboration between mathematicians and computer scientists, developing shared infrastructure and accelerating the use of AI in mathematical research.

At Carnegie Mellon, that collaboration is already underway. Serving among the leadership of the new institute, Avigad, Heule and Welleck work together to support the mathematics research community.

Expanding Access

The Lean community, supported by contributors around the world, has created an open and collaborative environment for formalized mathematics. Mathlib continues to grow as a shared resource, lowering barriers to entry for students and researchers alike. 

“One of the best things about Lean and Mathlib is the vibrant, supportive community that has sprung up around them,” Avigad said.

By allowing users to experiment with proofs and receive immediate feedback, systems like Lean offer a new way to engage with mathematical ideas.

Individually, each of these approaches — formalization, automated reasoning and neural AI — is powerful. Together, they form what researchers describe as a “full stack” for mathematical intelligence. Neural models can generate ideas. Automated systems can search for solutions. Formal tools can verify results with absolute certainty. 

“Each method has its blind spots. By merging them, we can let AI explore freely while still checking every step along the way,” Heule said.

This integration reflects a broader trend in AI, where hybrid systems combine strengths to overcome individual limitations. 

Looking Ahead

As AI continues to evolve, its role in mathematics is likely to expand. 

Researchers envision a future in which AI systems assist with everything from routine proofs to major discoveries, working alongside humans to push the boundaries of knowledge. 

For Avigad, the goal is not just technological advancement, but preserving the core values of mathematics in a changing landscape.

“There is a lot to worry about these days. We owe it to the next generation to figure out how mathematics should look in the age of AI, and how to keep mathematical reasoning central to our lives,” he said.