Maths Circle Lecture #1
Thanks to Professor Kevin Buzzard for delivering the first lecture in our annual Maths Circle series titled 'Can AI prove theorems?'
Kevin Buzzard, a professor of pure mathematics at Imperial College London, specialises in formal proof verification, which is an exciting field in mathematics. Kevin came to deliver a lecture on the future of AI in mathematics.
One of the highlights of his lecture was the IMO Grand Challenge—a groundbreaking attempt to build an AI capable of solving International Mathematical Olympiad (IMO) problems at a gold-medal level. What makes this challenge so interesting is that solving IMO problems requires more than a strong grasp of mathematical concepts. It involves a flash of brilliant insight, which today's AI finds hard to impossible. Buzzard, a key member of the IMO Grand Challenge team, explained the intricate rules governing this ambitious project, which can be explored further here.
Report written by Ethan (Year 12)
On Monday we were delighted to welcome Professor Buzzard of Imperial College once again who gave students from Wilson’s and other local secondary schools a great talk on the theorem proving capacity of AI. For the first part of his talk he enlightened us of what studying maths at university is actually like compared to the calculation-based maths that all of us have studied throughout our school careers – in fact, it is almost completely different!
After this introduction, Professor Buzzard began to talk more about the proofs that mathematicians have solved in the past such as the proof showing that there are an infinite number of prime numbers.
Now moving onto the main part of the talk, we were shown how AI has already been involved in multiple mathematical breakthroughs including those in knot theory and the use of the programming language “Lean” which, if able to compile the proof given, is able to confirm mathematical proofs that mathematicians have written. However, there is one problem that remains – what if we took away this human input? Through the rise of Natural Processing we have been able to create Large Language Models (LLMs) such as ChatGPT but its role in mathematics has one big issue – it can’t do maths!
Professor Buzzard then ended the talk with the state of AI in mathematics as it is at this very moment and the efforts being made to improve it in this way such as competitions where the aim is to produce LLMs to solve a series of maths problems as accurately as possible. Buzzard proposed the idea of combining the capabilities of Lean and the LLM to increase this accuracy and the current attempts of applying this have currently fallen short, such as only being able to solve 3 questions of the IMO!
But there is no need to worry, for our maths teachers’ jobs are safe… for now.
Report written by Felix (Year 12)
