Will AI Replace Mathematicians?

You are currently viewing Will AI Replace Mathematicians?

Will I be able to answer the question in the title?  Maybe not, but Dr. Kevin Buzzard might. Dr. Kevin is a mathematics professor at Imperial College London, where he takes an undergraduate mathematics course teaching students math in a very different way compared to how you and I have learned it traditionally.

THE MATHEMATICS

To realise what different mathematics means, let’s first look at our mathematical foundations. The classical mathematics we’re used to is based on set theory. Bertrand Russell believed that the whole of mathematics could be derived using set theory, and all objects can be defined using sets. He spent years developing, formalising, and creating such a system. Eventually,  Gödel came along and proved that there exist statements in every consistent mathematical system that can neither be proved nor disproved within that system. Bertrand’s vision remained a pipe dream. Still, his set-theoretic math works well for us and is extensively used.

Consider the definition of numbersthey are very intuitive to us but they are defined rigorously in set theory (“{}” is used to represent a set, and things between the curly braces are elements of the set).

0 is defined as an object used to represent the number of elements in the empty set (I won’t go into defining the empty set). 1 is defined as an object representing the number of elements in a set containing 0. 2 is defined as an object representing the number of elements in a set containing 0 and 1.

As you can see, this is a very creative way to define a number where the number represents a set that has the same “number” of elements in it. This definition comes from the Zermelo–Fraenkel (ZF) set theory.

Let’s look at another object; most of us are familiar with a function. A function ‘F’ is defined as follows:

Consider two sets, A and B. Now consider a set F, containing ordered pairs (x, y), where x will cycle through all the values from A, and y can be any element(s) from B.

As an example: let A = {1, 2, 3}, B = {a, b, c}, 

And F = {(1, a), (2, a), (3, c)}

F is defined as a function from A to B. Hence, even a function is a set in set-theoretic mathematics.

Although serving the purpose of practicality and formal definition, this definition does little to express the ‘idea’ of a function. 

A function is usually seen as the following:

This idea is not communicated explicitly in set-theoretic mathematics.

In this regard, set theory is quite “dry” where everything needs to be a set, and everything is of the same type.

Type theory to the rescue:

Without going into the nitty-gritty details of type theory, it works better at capturing the object’s essence. It also allows us to write proofs in a more programming fashioned way.

For example, in set-theoretic mathematics, you can make the statement, “Aliens either exist, or they don’t,” and prove it. Although being a correct statement, it tells us nothing about whether aliens exist or not. Type theory does consider such statements proven (they can still exist as unproven statements) until you either produce an alien or give conclusive evidence that one cannot exist. This signifies the constructive nature of dependent type theory.

This advantage results in a type of constructive mathematics, where you have to make objects (or give evidence of their existence/non-existence) as you use them. People familiar with programming in any top-down OOP language (e.g., C++) know this because there, you have to predefine variables and their types (integer, float, etc.).

So how does this help make an AI?

Enter Lean.

Lean is a programming language and framework where you prove mathematical (or other) statements using type theoretic mathematics. Lean draws from and stores proofs in a big community-driven database called mathlib (short for math library), a library where people contribute proofs of existing mathematical literature written in Lean.

While writing a proof in Lean, you can draw from thousands of other proofs already submitted and verified by Lean. The system has an internal kernel that can handle simple logic. So, you break up your proof into bits and pieces, and Lean verifies them along the way.

Another advantage this gives us over set theoretic mathematics is that with set theoretic math, when someone writes a long and complicated proof, it takes a lot of time and effort of others to review and check its soundness. This was famously the case with Andrew Wiles and his initial proof of Fermat’s Last Theorem. Wiles records that, “…sometime in September I began to realise that this wasn’t just a minor difficulty but a fundamental flaw. It was an error in a crucial part of the argument involving the Kolyvagin-Flach method, but it was something so subtle that I’d missed it completely until that point. The error is so abstract that it can’t really be described in simple terms. Even explaining it to a mathematician would require the mathematician to spend two or three months studying that part of the manuscript in great detail.” This type of situation can be embarrassing for the author and time-consuming for the math community in general. 

Professor Gadgil, IISc Bangalore, on Set vs. Type Theory:

I too think that type theory (specifically dependent type theory) is much better than set theory (more precisely First-Order Logic + Set Theory), and that Lean prover is very well designed, 8*especially if one considers the “lean prover ecosystem.”

Lean’s use of type theoretic mathematics, the kind with distinguishing features including focussing on the evidence alongside and utilising the logic unit, results in the construction of correct proofs only. 

Lean also provides a central database for organising the entirety of mathematical literature; you can instantly draw from these proofs into your proof as Lean has learned all of them. Lean can even suggest proofs to you based on the hypothesis you make inside it. This suggestion feature, along with the logic unit, comprises what is called a proof assistant. This, as the name suggests, assists the mathematician and streamlines the proof-writing process.

—–

Note on proof assisters:

I will take the liberty to mention that Lean is not the only proof-assister that uses type theory. To generalise further, type theory is not the only framework that allows proof-assisters. There have been other proof-assisters:

  • Coq: (1989) Based on type theory. It is more of a proof management system than an actual proof-assister which is still used by many today. Last stable release: 11 December 2020
  • Isabelle: (1986) A proof assistant that operates on HOT (higher-order logic) and accepts set theoretic proofs. Last stable release: April 2020
  • Mizar: (1973) Based on set-theory. The distinguishing feature is its readability, with syntax derived from mathematical vernacular. Last stable release: June 2019

—–

No. of files contributed to Lean as of 30th Dec 2020

As of today, people from all over the world have contributed over 43,000 proofs to the Lean library in various fields of mathematics.

The ultimate goal for Lean then would be to build an artificial intelligence system that not only proves or disproves a hypothesis we give it but even comes up with theorems on its own.

Still, we must not get too ahead of ourselves. I had the opportunity to hear back from Dr. Kevin Buzzard, who, as mentioned in the first paragraph, uses Lean in his undergrad course at ICL, and these were his words:

“Some of us believe the dream that one day software such as this will help the modern mathematician in the same way that usual math packages help them, but I would not be surprised if people have been dreaming this for 30 years and one certainly can’t argue that it’s happening right now, Lean has given me some insights into undergraduate teaching but has told neither me nor anyone else anything useful about the Langland’s philosophy (a complex mathematical problem) or anything else fancy.

We can dream but it wouldn’t surprise me if people have been dreaming for decades. What’s different here is that it seems to me that a whole bunch of what I would snobbishly refer to as “proper mathematics” (e.g., all the advanced BSc and MSc algebra going into Lean right now) is all currently appearing in one library in one system, so at the very least the groundwork is being done to make some sort of system which might be able to help people do MSc level algebra in some way. This didn’t seem to be happening before, other systems just have a bunch of disparate projects with no underlying goal. But whether this will be a game changer very much remains to be seen.”

So, we do realise we probably can’t expect the AI soon enough.

Dr. Siddhartha Gadgil, Dept. of Mathematics, IISc Bangalore, the leading figure in the field of proof assisters in India, has developed his own proof-assister, ProvingGround, based on type-theory and written in Scala. He also has numerous international collaborations related to this field, most notably the Polymath 14 project, in which some mathematicians (including Fields medallist Terrence Tao) and a computer worked together to generate a proof for a mathematical problem.

Dr. Gadgil was generous enough to answer some of our questions:

Q: How did you get into the subject (proof-assisters)?

I started working on this because I felt it was interesting, worthwhile and it was at a stage where it could grow fast. There was no particular trajectory for me to get to this.

Q: How useful is it to mathematicians (or can be) according to you?This depends of course on how good the system is, and also how usable it is. But even if we make only partial progress, one should be able to develop “semantic tooling” for mathematics. For instance, MathSciNet (a mathematical journal library) searches are based purely on text, not the meaning of contents/abstracts of papers. As I have become familiar with software tooling, this seems downright primitive. One should hope that when working on a question, a chat bot or IDE (i.e., fancy editor) should be able to find related results searching by meaning, automatically do some experimentation to test conjectures, etc.