Verifying the correctness of mathematical theorems with a computer
How correct are mathematical theorems? And is all the theory around them correct? To find out, mathematics student Dominique Lawson converted a mathematical theorem into computer language. ‘This allows a computer to understand the theorem and check whether the proof behind it is entirely correct.’ The research got him a nomination for the faculty award Young Talent 2023.
Having a computer check whether a mathematical theorem is correct is called formalisation, Dominique explains. ‘You have to work very precisely for this, because the proof may not contain any gaps.’ Dominique researched a theorem within the field of directed topology. ‘This is a relatively new branch of mathematics that has applications in concurrency, for example. That is a branch of computer science that delves into concurrent execution of programs.’ The computer could not find any holes in Dominique's theorem. ‘It has now been fully verified by a computer that this theorem is correct.’
‘They are proof assistants’
In recent years, there has been an increasing interest in formalising mathematics. ‘Computers can help to write proofs for a mathematical theorem. So they are like proof assistants,’ says Dominique. ‘Mathematicians only have to think of the big picture and the software works out the details. It's nice if a lot of mathematics has already been formalised, because then you can use previous results.’
Another big advantage of formalisation is the guarantee that everything is correct. ‘It sometimes happens that someone publishes something that others doubt is correct. A computer-verified proof then offers a solution.’
Mathematical concepts from a different angle
Formalising mathematics was new to Dominique. ‘I hadn't come across it during my undergraduate. I really liked this refreshing method of programming with mathematics. You suddenly look at many mathematical concepts from a completely different angle. It is also wonderful to be sure that the result is correct. If there would be bugs or errors in it, the programme immediately alerts you.’
The student, who is now in the first year of the Master of Mathematics, looks back on his research with great pleasure. ‘When you finish a part, a message appears on your screen saying: goals accomplished with a confetti emoji. That makes writing this more fun after all. And when the very last part of my research was completed, that confetti emoji felt very much deserved.’