Recent advances in AI have brought us closer to building autonomous AI mathematicians capable of formulating conjectures, constructing proofs, and discovering mathematical knowledge. Yet, as statistical models, large language models (LLMs) lack built-in guarantees of logical correctness. Formal methods offer a bridge between statistical intelligence and rigorous mathematical reasoning, enabling LLMs to formulate, examine, and develop mathematical ideas within formally defined and verifiable frameworks. In this talk, I will discuss three ongoing projects that explore how formal methods can support these capabilities. First, I will introduce structure-aware equivalence, which provides a principled approach to assessing the semantic correctness of auto formalized mathematical statements. Second, I will present a complementary framework based on property-based testing, which searches for counterexamples to potentially incorrect formalizations and uses Lean to certify the refutation. Finally, I will discuss our preliminary work on autonomous axiomatization, where AI systems attempt to discover and refine axiomatic theories through observations, deductive reasoning, and theory evaluation. Together, these projects illustrate how formal methods can go beyond verifying AI-generated proofs to actively guide mathematical reasoning and discovery. More broadly, they motivate a research direction toward AI mathematicians that can not only prove theorems, but also rigorously examine, revise, and extend the mathematical theories they work with.
About Yuxiang Peng
Yuxiang Peng is an Assistant Professor in the Department of Computer Science at Purdue University. His research focuses on theoretical and practical explorations of high-assurance software toolchains for quantum computing, including programming languages, compilers, and systems. His research goal is to advance the frontier of and help common users harness the power of modern quantum computers and other emerging computing instruments in various domain problems, such as optimization.