Proof assistants
An exciting new development in mathematics is the invention of proof assistants. Proof assistants ensure that the mathematics that is produced is grounded in the axioms that should underpin them. Whilst it is still early days, it is an exciting time, especially when coupled with the idea that AI could use these proof assistants to begin reliably checking and producing maths!
This collection came from following up with Kevin Buzzard, a Professor of Pure Mathematics at Imperial College London, after a 2025 workshop at the Isaac Newton Institute for Mathematical Sciences (INI) called Big Proof. This followed on from a 2017 research programme on the same topic, which was very much ahead of its time.
Proof assistants
In this article we introduce what a proof assistant is and look at some examples where they have been used.
Proof assistants (part 2)
Continuing on from part 1, we explore how proof assistants are boosting the mathematical community and how they could be used in conjunction with large language models.
Maths in a Minute: Coding with Lean
See a walkthrough of how a proof assistant is used for a simple example.
Kevin Buzzard and Big Proof
Listen to Kevin talk to us about proof assistants in this episode of our Maths on the Move podcast.
Some background and further reading
This isn't the first time we at Plus have interacted with Buzzard, with him commenting on why he sees pure mathematics in crisis in an earlier article. There are also several other articles that look at the nature of proofs in the modern day.
Pure maths in crisis?
In this article from 2019 Buzzard explains why he thinks that the standard of proof in research maths might not be as high as mathematicians would like to believe.
How to (im)prove mathematics
This article explores how the simple notion of counting ends in a revolutionary new way of doing maths using proof assistants. This article is based on a talk by Terence Tao at a 2024 workshop at the INI which celebrated the mathematics of Tim Gowers as well as his 60th birthday.
Welcome to the maths lab
This article from our archive explores the state of affairs regarding computer assisted proofs back in 2004. You will meet the famous Four Colour Theorem and a generalisation of Kepler's conjecture.
To find out more about a couple of the results mentioned in the articles above see the following articles.
A very old problem turns 30!
This article explores Fermat's famous last theorem as well as the mathematics its proof has given rise to. It comes with a podcast featuring Andrew Wiles, who proved the result, and people who are now working on its legacy.
The origins of proof IV: The philosophy of proof
This article from 2000 looks at Fermat's Last Theorem, the Four Colour Theorem, and Kepler's conjecture, each of which are relevant to our topic of computer assisted proofs.
Are you feeling curious about the axioms that mathematicians use to build up all of the beautiful mathematics that we see all around the world? Have a quick dive into the Maths in a Minute articles below.
Maths in a minute: Peano arithmetic
Counting, adding subtracting — these are natural things to do for us humans, but how would you explain them to an alien? Here are some axioms to help you along.
Maths in a minute: Euclid's axioms
Perhaps the most famous set of axioms of them all relates to geometry and is down to the ancient mathematician Euclid of Alexandria.
This content forms part of our collaboration with the Isaac Newton Institute for Mathematical Sciences (INI) – you can find all the content from the collaboration here.
The INI is an international research centre and our neighbour here on the University of Cambridge's maths campus. It attracts leading mathematical scientists from all over the world, and is open to all. Visit www.newton.ac.uk to find out more.
