Why should you care about proof assistants?

Let’s start with a definition. A proof assistant (or interactive theorem prover) is a computer program that helps users create and check proofs using formal methods (see: type theory). Examples of popular proof assistants include Lean, Rocq and Isabelle.¹ The best thing about theorem provers is that they guarantee the correctness of a proof.

As far as I know, you can use a proof assistant in at least four cases:

1. You enjoy it;
2. You really care about the certainty and reliability of your software;
3. You are doing research at the intersection of mathematics and AI;
4. You are teaching (or learning) formal mathematics.

I will briefly describe these reasons.

Enjoyment#

Some people (like me) simply enjoy writing formal proofs. Some (like Terence Tao) see proof assistants as a great way to collaborate (because you don’t need to check the work of others — the theorem prover does it for you).

Two of the coolest projects (besides standard libraries, like Lean’s Mathlib) are The Busy Beaver Challenge and The Equational Theories Project. Terence Tao, mentioned above, started the latter and recently gave a great talk about it, which I highly recommend: The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale (from the 2025 Big Proof workshop).

Software reliability#

You can write formally verified software instead of writing tests. It usually takes much longer to code, but sometimes it is worth it, especially when you can’t sufficiently test all possible cases. There are already some very advanced verified programs, including:

• CompCert, a C compiler;
• HACL*, a full-blown cryptographic library;
• seL4, an OS kernel;
• and even very recent approaches to full OS verification.

Mathematical research#

You may have heard that AI achieves gold-medal standard at the International Mathematical Olympiad (IMO). It all kind of started with theorem provers. Arguably, the first major result of combining AI and proof assistants for math was AlphaGeometry. Since then, there have of course been some advances, including 4 research teams claiming the gold medal for their AI models at the IMO 2025:

• OpenAI’s experimental model (used reasoning LLM), see the very strange proofs;
• Gemini Deep Think from Google DeepMind (used reasoning LLM), proofs;
• Harmonic’s Aristotle (used Lean), proofs;
• Seed-Prover from ByteDance (used Lean), proofs.

ByteDance (yes, the TikTok company) was the only one kind enough to give us a paper instead of a press release.

As a side note, see this mastodon thread from Terence Tao.

A great introduction to today’s state-of-the-art methods and directions for future research (not necessarily IMO-centered) is a talk AI for Mathematical Discovery: Symbolic, Neural, and Neuro-Symbolic Methods given by Moa Johansson as a keynote at the 2025 Lambda Days conference.

Teaching mathematics#

There is some evidence suggesting that learning to use interactive theorem provers can be beneficial for students at the beginning of their university-level mathematics education. Fortunately, there are plenty of accessible learning resources available — one engaging example is the Natural Number Game. I hope this post has been compelling enough for you to give it a try.