We are well aware that computers have changed our lives over the past three decades. In the case of mathematics, they started doing so even before personal computers existed. The first computer-assisted proof was published in 1970. The computer was programmed to go through thousands of cases to prove the ‘four-colour theorem’. But when it comes to computer-generated proofs – actually proving theorems from scratch – computers are way behind humans.
With recent developments in artificial intelligence (AI), the wind seems to be changing. The first sign was in 1997 when IBM’s Deep Blue defeated then chess champion Kasparov with a brute force approach. Then in 2017, Google’s AlphaGo defeated current Go champion Ke Jie, followed in the same year with AlphaZero defeating other computer programmes with a novel reinforcement-learning algorithm.
Mathematics itself can be seen as a sort of game in which ‘checkmate’ is some unproved conjecture (such as the Riemann hypothesis or the Goldbach conjecture) and the rules of the game are the manipulation of symbols using logic. In reality, it is not so easy.
What has been feasible for some time is a much lower target, that of a ‘computer proof assistant’ which takes a given proof as input and checks whether all the steps are correct. One of these, HOL, developed at Cambridge University, has been used to formally check the Jordan Curve theorem, which is so hard very few undergraduate courses attempt to prove it.
Another of HOL’s recent (2017) successes is the verification of the Kepler conjecture supposedly proved in 1998 by Thomas Hales, but which was so complicated that, since then, no one could vouch for its veracity. Proofs are, with the passage of time, becoming more complicated. Two years ago, there appeared a paper by Norbert Blum that claimed P≠NP, thus resolving a conjecture in the list of seven Millennium Prize problems. But, again, it took more than a year to realise there was a subtle mistake because the ideas are so complex. Computer-verified proofs are very likely to become the new standard for publication.
The major problem is that a submitted proof must be completely formalistic, not written in English. Although there are converters, they commit enough errors in a long proof that the conversion becomes next to useless. Secondly, all the formal verified theorems need to be gathered into a library so that they can be retrieved at will. But both obstacles will be overcome eventually.
The next step up is that of an interactive ‘theorem prover’. There are already some freely available ones, including HOL Light, written by Cambridge University researchers (https://www.cl.cam.ac.uk/~jrh13/hol-light/ and https://hol-theorem-prover.org/), and its neural network version DeepHol, Microsoft’s Lean, and Coq, written by researchers from several French universities. They use ideas from artificial intelligence, where the programme throws up suggestions to follow and mathematicians decide which avenues to follow. At present they are complex enough to be able to solve undergraduate exercises, but at the rate they are improving they will become essential tools for mathematicians in a few decades.
Mathematician Timothy Gowers, a Fields medallist at Cambridge University, predicts that by the end of the century, computer provers would have supplanted mathematicians. Science fiction visions of a HAL-type computer taking over humanity may be nothing more than mirages or nightmares, but even specialised versions of AI-assisted software will wholly supplant the way we learn, teach, and research university subjects.
Joseph Muscat is a professor at the Department of Mathematics at the University of Malta.
Did you know?
• 1 + 2 + 3 + 4 + 3 + 2 + 1 = 4²
1 + 2 + 3 + 4 + 5 + 4 + 3 + 2 + 1 = 5² etc.
• There was a mathematical Twitter storm this summer because of a formula that seems to have two correct answers: 8÷2(2+2). Teachers who swear by BIDMAS were caught out disagreeing with their US counterparts, who, as it turns out, use a different rule called PEMDAS.
• If A does not imply B then B implies A. This can be seen from its truth table:
| A | B | A➯B | B➯A | NOT(A➯B) |
| ➯ (B➯A) |
| T | T | T | T | T |
| T | F | F | T | T |
| F | T | T | F | T |
| F | F | T | T | T |
Of course, we know from experience that this cannot be valid: “If a cough does not imply fever, then fever implies a cough” is utter nonsense. Send your ideas for resolving this conundrum to joseph.muscat@um.edu.mt, to be published in my next article.
• Quote from the mathematician Andre Weil to the renowned film director Akira Kurosawa: “I have a great advantage over you: I can love and admire your work, but you cannot love and admire mine.”
For more trivia, see: www.um.edu.mt/think
Sound bites
• International scene: Which three cubes sum up to 99? That’s easy: 2³+3³+4³. For 6 you have to think harder but it can be done: 2³+(-1)³+(-1)³=6. By last year all numbers up to 100 that have a solution were solved, except for 42 (which is the ultimate number for Hitchhiker’s Guide fans). This has also succumbed last month using a supercomputer programmed by Andrew Sutherland (MIT) and Andrew Booker (Bristol):
(-80538738812075974)³ + 80435758145817515³ + 12602123297335631³ = 42.
Try your luck with the next two unknown numbers: 114 and 165.
Local scene: Think of a computer algorithm outputting numbers that home in on some value, for example, the square root of 2. A generalisation of this leads to considerations about how information is acquired. It can only be gained incrementally in finite steps, but it can be lost without restriction. The research paper ‘An Axiomatization of Filter Clustering’ by Joseph Muscat, presented at the 12th International Conference on Fuzzy Systems and Knowledge Discovery in 2015, is a rigorous formalisation of these concepts.
For more sound bites, listen to Radio Mocha: Saturday at 7.30pm on Radju Malta and Monday at 9pm on Radju Malta 2 (https://www.fb.com/RadioMochaMalta).