There are ongoing rapid advances in the power and versatility of AI or artificial intelligence. Computers are now producing results in several fields that are far beyond human capability. The trend is unstoppable, and is having profound effects in many areas of our lives. Will mathematicians be replaced by computers? [TM195 or search for “thatsmaths” at irishtimes.com].
Let us reflect on what has happened in other areas. Early computer-generated music was crude; the composer’s job was safe. Now computers produce compositions with the intricacy of a Bach fugue, difficult to differentiate from “the real thing”. The first attempts to translate language using computers were pathetic; now machine translation is invaluable. Years ago, we were confident that a computer would never beat a Chess Grand Master; now machines are unbeatable. It’s the same story for the subtle board-game Go.
The Role of Computers
A leading mathematician Paul Halmos opined decades ago that computers had no role in pure mathematics. Around the same time, the renowned logician Paul Cohen expressed the view that at some future time research mathematicians will be replaced by computers. Nobody knows for sure, but the truth is likely to lie somewhere between these extremes: the computer will generate candidate conjectures, and produce theorems or refutations, while human intuition will determine which candidates are interesting and should be explored more deeply and which appear sterile and can be disregarded.
What is this mathematical intuition? Intuition is insight that does not depend on rigorous reasoning. It guides us towards plausible results in the absence of proof. It is holistic rather than analytical. It is essential in the creative process of mathematics. But in the end, a result arising through intuition remains a conjecture until a rigorous proof is found. There are many sparkling conjectures crying out for some brilliant mathematician to prove them.
Axiom, Theorem, Proof
Mathematics is often viewed as a deductive science: assumptions (axioms) are made and the laws of logic are applied to deduce consequences (theorems). But possible theorems are conjectured by induction: intuition, guesswork, trial and error and experimentation have a central role. The process of proving a theorem by systematic application of logical rules is simple to mechanise; computers are ideally suited to carry out symbolic manipulations that lead from the initial hypotheses to the conclusion, producing a proof.
However, the best proofs involve brave leaps of imagination based on intuition. These are far more difficult to reduce to blind, plodding rules. On the other hand, computers can analyse millions of published proofs – many more than a research mathematician – and uncover patterns of reasoning and successful strategies for progress. Ultimately, this incredible power is bound to win out over human limitations, just as it already has for chess and Go.
Theorem Provers
Computer programs for proving theorems come in two distinct types. There are automated theorem provers (ATPs) which perform prodigious computations, crunching out long sequences of logical steps leading from the axioms to the conclusions. Once written, they work without any human intervention. They have been successful in proving some results that have defeated researchers. In contrast, interactive theorem provers (ITPs) are used by mathematicians to assist in proofs. These proofs require a combination of creative thinking and meticulous mechanical reasoning. An ITP can carry out the laborious tasks, while the mathematician provides the creative insights.
Computers have helped with some important mathematical advances: the four-colour theorem and Kepler’s conjecture both required intensive computation for their proof. There has been argument amongst mathematicians about these proofs, since detailed checking of them is beyond human capacity. Another difficulty is that computers can generate proofs that are difficult or impossible to understand. How does that bear on their veracity?
Controversial
Views on the role of computers remain controversial. Undoubtedly, they have a role in checking proofs and in deciding on the validity of theorems submitted for publication. Many mathematicians are unenthusiastic about them, favouring the methods they have always used. While they see a role for the more mundane stages in a proof to be mechanised, they doubt if a computer can ever generate interesting conjectures. They argue that this creativity is a fundamentally human activity, impossible to automate. My own feeling is that rapid advances are inevitable and the role of research mathematicians will change dramatically.
Sources
Ornes, Stephen, 2020: How close are computers to automating mathematical reasoning? Quanta Magazine, August 27, 2020.
AweSums: Online Maths Course
One advantage of the pandemic is that university courses that were delivered through lectures are now available throughout the world, online via Zoom sessions. A UCD Zoom course, on recreational mathematics, AweSums: Marvels and Mysteries of Mathematics, will be presented by Prof Peter Lynch, School of Mathematics & Statistics, UCD. Registration is now open HERE.
ThatsMaths 