There's been a lot of talk recently about whether artificial intelligence is becoming just as good as maths as humans are. But quietly in the background there's been another development regarding the use of computers in maths. It involves proof assistants: computer programmes that can check whether a mathematical proof is correct; whether it can be derived from a set of basic axioms of mathematics using only the rules of logic.

In this episode of Living proof we meet Kevin Buzzard, an expert on proof assistants at University College London. Kevin explains what proof assistants are, how using them is like playing a computer game, and why they turn maths into a highly collaborative pursuit. He also tells us about his effort to get a proof assistant to check one of the most famous results in all of mathematics — Fermat's Last Theorem — and how proof assistants and AI may team up to provide a powerful tool.

We met Kevin in the summer when he was taking part in a research programme called Big Proof at the Isaac Newton Institute for Mathematical Sciences (INI) in Cambridge. This programme, which attracted some of the best minds in modern mathematics, followed on from a pioneering workshop on the same topic which took place at the INI in 2017.

To find out more about the topics mentioned in this podcast, see the following articles:

• Proof assistants — This two part article, written by our brilliant summer intern Ben Watkins, is based on the interview with Kevin Buzzard and explores what proof assistants are.
• Maths in a Minute: Coding with Lean — Here's a simple walk-through of how to use a proof assitant called Lean.
• Pure maths in crisis? — In this article from 2019 Kevin 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.
• 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.
• You can find more background reading in our collection on proof assistants.

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.

Earlier this year the the anomalous mathematical patterns sci-art competition attracted some jaw-dropping entries. The competition was held in connection to the Stochastic systems for anomalous diffusion research programme which took place at the Isaac Newton Institute for Mathematical Sciences (INI) in Cambridge last year.

In this episode of Maths on the Move we talk to Codina Cotar, who co-organised the INI programme and helped put on the competition. Codina explains the maths which served as inspiration and discusses some of the winning entries. From coffee to quantum mechanics and from dance to diffusion, find out how mathematics, nature and art are inextricably linked.

Note that the in-person exhibition at the INI is now scheduled for March 2026.

The entries discusses in this podcast are shown below. To find out more about some of the mathematical topics mentioned in this podcast see:

• The Sci-art competition - This article explores some of the mathematics behind the competition, including randomness, diffusion, and many particle systems.
• The Fields Medals 2022: Maryna Viazovska - This article looks at the mathematics of sphere packings, which won a Fields Medal for the mathematician Maryna Viazovska.
• Maths in a Minute: Fluid dynamics - A very bried introduction to the mathematics of liquids and gases.
• A ridiculously short introduction to some very basic quantum mechanics - This article does what the title suggests.
• A brief history of quantum field theory - A deeper look at the theory that arose from quantum mechanics.

Dye Diffusion in Water by Henrique Biasi. Find out more here.

A microcosm of milk by Christian Casaljay. Find out more here.

Work by Lilia Bakanova, which which won the category for textile, sculpture and other medium. Find out more here.

In this episode of the Living Proof podcast we're delighted to meet Moustapha Fall. Moustapha is the Center President of the African Institute for Mathematical Sciences (AIMS) in Senegal and winner of a prestigious Ramanujan Prize for Young Mathematicians from Developing Countries. He also plays an important role on the international stage as Member-at-Large of the Executive Committee of the International Mathematical Union.

Moustapha talks to us about about the amazing institution that is AIMS, about his outreach activities and advice for budding mathematicians, and about the challenges that face mathematicians in sub-Saharan Africa.

You can find the IMU-ICIAM report on fraudulent publishing, which Moustapha mentions in the podcast, here. The same team of authors has also drawn up recommendations on how to fight fraudulent publishing.