Automating Mathematics?

Siddhartha Gadgil

Department of Mathematics

Indian Institute of Science

Bangalore

http://math.iisc.ac.in/~gadgil/

https://github.com/siddhartha-gadgil/ProvingGround

		1997
		2017
	?	Whether? When? How?

What is Mathematics?

Prime numbers

A prime number is a number with exactly two factors, $1$ and the number itself.
For example, $3$, $5$ and $7$ are primes but $4$ is not a prime as it has factor $2$.
Primes are a basic object of study in Mathematics.
We will discuss what we study first, and then why.

How many primes?

901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000

9901
9902
9903
9904
9905
9906
9907
9908
9909
9910
9911
9912
9913
9914
9915
9916
9917
9918
9919
9920
9921
9922
9923
9924
9925
9926
9927
9928
9929
9930
9931
9932
9933
9934
9935
9936
9937
9938
9939
9940
9941
9942
9943
9944
9945
9946
9947
9948
9949
9950
9951
9952
9953
9954
9955
9956
9957
9958
9959
9960
9961
9962
9963
9964
9965
9966
9967
9968
9969
9970
9971
9972
9973
9974
9975
9976
9977
9978
9979
9980
9981
9982
9983
9984
9985
9986
9987
9988
9989
9990
9991
9992
9993
9994
9995
9996
9997
9998
9999
10000

How about twin primes?

901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000

9901
9902
9903
9904
9905
9906
9907
9908
9909
9910
9911
9912
9913
9914
9915
9916
9917
9918
9919
9920
9921
9922
9923
9924
9925
9926
9927
9928
9929
9930
9931
9932
9933
9934
9935
9936
9937
9938
9939
9940
9941
9942
9943
9944
9945
9946
9947
9948
9949
9950
9951
9952
9953
9954
9955
9956
9957
9958
9959
9960
9961
9962
9963
9964
9965
9966
9967
9968
9969
9970
9971
9972
9973
9974
9975
9976
9977
9978
9979
9980
9981
9982
9983
9984
9985
9986
9987
9988
9989
9990
9991
9992
9993
9994
9995
9996
9997
9998
9999
10000

Arithmetic progressions in primes

An arithmetic progression is a sequence of numbers so that the difference between two consecutive terms is constant, for example
- 5, 7, 9, 11.
- 4, 7, 10, 13, 16.
- 11, 17, 23, 29.
We consider prime arithmetic progressions, like the third example.
For experiments, we take the first million pairs of primes and extend to maximal prime arithmetic progressions.

Some prime arithmetic progressions of length $3$:
There are $110386$ of these among the first million.

Some prime arithmetic progressions of length $4$:
There are $27836$ of these among the first million.

Some prime arithmetic progressions of length $5$:
There are $3665$ of these among the first million.

Some prime arithmetic progressions of length $6$:
There are $980$ of these among the first million.

Some prime arithmetic progressions of length $7$:
There are $127$ of these among the first million.

Some prime arithmetic progressions of length $8$:
There are $46$ of these among the first million.

6947

13877

20807

27737

34667

41597

48527

55457

137

8117

16097

24077

32057

40037

48017

55997

63977

409

619

829

1039

1249

1459

1669

1879

2089

433

3583

6733

9883

13033

16183

19333

22483

25633

1699

5689

9679

13669

17659

21649

25639

29629

33619

2063

3323

4583

5843

7103

8363

9623

10883

12143

3499

3709

3919

4129

4339

4549

4759

4969

5179

3823

6133

8443

10753

13063

15373

17683

19993

22303

4721

7451

10181

12911

15641

18371

21101

23831

26561

6043

6883

7723

8563

9403

10243

11083

11923

12763

There are $15$ prime arithmetic progressions of length $9$ among the first million.

There is just $1$ arithmetic progressions of length $10$ among the first million.
The largest explicitly known arithmetic progression is of length $27$.

Lengths of arithmetic progressions

For the first million pairs of primes, lengths of the maximal prime arithmetic progressions are:

length	2	3	4	5	6
number	856944	110386	27836	3665	980
length	7	8	9	10
number	127	46	15	1

The largest explicitly known arithmetic progression is of length $27$.

Some questions

Question: Are there infinitely many primes?
Answer: Yes, as proved by Euclid.
Question: Are there arbitrarily long arithmetic progressions of primes?
Answer: Yes, by the Green-Tao theorem from 2004.
Question: Are there infinitely many twin primes?
Status: We still do not know.

What is the use?

Occasionally, a mathematical result finds unexpected applications.
Far more often, in finding the answers to mathematical question we discover concepts, i.e., ways of looking at the world, which are useful.
For example, Gauss developed the concept of intrinsic curvature motivated by a geodetic survey.
This was further developed, and generalized to higher dimensions, by Riemann.
Einstein's general relativity was based on intrinsic curvature (as is the Berry phase).

Mathematical Proofs

Infinitude of primes

Lemma: Every number $n > 1$ has a prime factor.
Proof: Let $p > 1$ be the smallest factor of $n$ that is bigger than $1$.
Then $p$ must be a prime as
- Suppose $q > 1$ is a factor of $p$, then $q$ is a factor of $n$ and $q \leq p$.
- But $p$ is the smallest factor of $n$ that is bigger than $1$, so it must be that $q = p$.
- So the only factors of $p$ are $1$ and $p$, i.e., $p$ is a prime.

Infinitude of primes II

Lemma: For any positive number $n$, there is a prime bigger than $n$.
Proof: Let $m = n! + 1$, where $n!=1\times 2\times3\times\dots\times n$ and let $p$ be a prime factor of $m$.
Then $p$ must be greater than $n$, as, if $p \leq n$,
- $p$ divides $n!$, and
- $p$ divides $n! + 1$, which means
- $p$ divides $(n! + 1) - n! = 1$, which is absurd.

Formal Mathematical Proofs

A formal proof is a finite sequence of sentences, each of which:
- is an axiom (something we believe true about the universe), or
- is an assumption, or
- follows from the earlier sentences by a rule of inference.
A formal proof can be checked mechanically.

Formal proof in Mizar

reserve n,p for Nat;
theorem Euclid: ex p st p is prime & p > n
proof
set k = n! + 1;
n! > 0 by NEWTON:23;
then n! >= 0 + 1 by NAT_1:38;
then k >= 1 + 1 by REAL_1:55;
then consider p such that
A1: p is prime & p divides k by INT_2:48;
A2: p <> 0 & p > 1 by A1,INT_2:def 5;
take p;
thus p is prime by A1;
assume p <= n;
then p divides n! by A2,NAT_LAT:16;
then p divides 1 by A1,NAT_1:57;
hence contradiction by A2,NAT_1:54;
end;
theorem {p: p is prime} is infinite
from Unbounded(Euclid);

The full formal proof is 44 lines

Verifying a formal proof is purely mechanical.
However, to find the proof, in addition to (mechanical) computations and deductions,
- We stated useful lemmas, or judged that previously known results were useful.
- We considered the smallest factor $> 1$, conjectured and proved the statement that it was prime.
- We considered (a prime factor of) $n! + 1$, based on backward reasoning.
It is hard to formulate rules for these steps.

Puzzles, Games, Reasoning

Puzzles

Some puzzles: jigsaw, sudoku, detective stories, quiz questions, planetary motions, ...
A puzzle is a precisely stated problem for which
- it is (fairly) easy to check that a solution is correct, but
- it is hard to find the solution.
A solution may be formal or informal.
We solve puzzles by a mixture of deduction (algorithms) and intuition.

Deductive reasoning/Algorithms

We perform a small number of steps, each step a calculation or move or deduction.
The steps are based on a small number of rules (possibly depending on a small number of parameters).
A computer's notion of small is very different.
We can try to solve harder problems by inventing better algorithms: multiplication with carry-over, fingerprints, SMT solvers.

Tacit knowledge & Intuition

Tacit knowledge is the kind of knowledge that is difficult to transfer to another person by means of writing it down or verbalizing it.
Examples: riding a bicycle, speaking a language.
Experts have a lot of tacit knowledge, typically learned through experience.
Intuition is based on tacit knowledge.
While intuition is sometimes wrong, to be useful it should be correct often enough.
- A hunch is sometimes correct.
- A judgement is often correct.

Solving puzzles

Checking a solution should be purely deductive.
However, finding a solution involves:
- deciding what to consider - a policy, which may use intuitive hunches, and
- deciding how promising the present approach/situation is - the value, which may use intuitive judgements.
A computer following a purely algorithmic approach can compensate by following up on far more approaches, and looking for consequences further ahead before deciding the value.

Computers and Games

Rewards, values and policies

The rules of a game (e.g. chess) tell us
- what moves we can make.
- what reward we get at a stage - e.g. win/loss/draw at the end.
In tic-tac-toe, we can simply calculate the reward.
In most cases however, we need
- A policy - what moves to consider.
- A (relative) value telling us what future reward we can expect based on the present position.

Kasparov vs Deep Blue

In Chess, a basic value is obtained by counting pieces and pawns with weights.
Standard openings also give a policy during the early stages of the game, as do endgame tables.
Deep Blue, and chess theory, extend these to elaborate (rule based) values and policies.
The value and policy functions of Kasparov were far better, but compensated for by Deep Blue being able to consider far more move sequences.

AlphaGo vs Lee Sedol

In the chinese game Go, the number of legal moves is much larger, so trying everything means we cannot look many moves ahead.
More importantly, it is very hard to describe a good value function.
This makes it far harder for computers.
Yet, in March 2016, a Go playing system AlphaGo defeated 18-time world champion Lee Sedol.
In January 2017, AlphaGo defeated the world number one Ke Jie comprehensively.

AlphaGo and Learning

The policy and value functions of AlphaGo are deep neural networks that were trained.
The policy network was trained by learning to predict the next move from games of expert players.
The value network was trained by AlphaGo playing against versions of itself.
AlphaGo considered fewer sequences of moves than Deep Blue.
AlphaGo came up with unexpected moves.

AlphaGo Zero and Alpha Zero

AlphaGo was succeeded (and defeated) by AlphaGo Zero, which learnt purely by self play.
Its successor, AlphaZero, could master a variety of similar games starting with just the rules.
AlphaZero took just 4 hours to become the strongest chess player on the planet (beating a traditional chess program, Stockfish).
AlphaZero “had a dynamic, open style”, and “prioritizes piece activity over material, preferring positions that looked risky and aggressive.”

Artificial Intelligence elsewhere.

Word Embeddings

To give words a structure and capture relations, words are embedded as points in space.
To do this, (in Word2Vec) we set up the problem of predicting a word given its neighbours.
We look for solutions of this problem that involve mapping words into space, and predicting from neighbours using the points.
Analogies such as Paris is to France as Berlin is to Germany are captured by vector operations.

Generative Query network

In an artifical 3D environment, the network observes 2D images from a few positions.
It has to predict the observed image from a new position.
To do this, the 2D image was mapped to a concise representation by a network, which was then used to predict the image from a different viewpoint.
The concise representation factorized by colour, shape and size (among other things).

Generative Adversarial Network

These consist of a pair of networks, contesting with each other.
One network generates candidates (generative) and the other evaluates them (discriminative).
For example the discriminative network tries to distinguish between real images and synthetic ones generated by the generative network.

Distributional reinforcement learning

In temporal reinforcement learning, a network tries to predict (average) future rewards.
However, sometimes the reward is either very big or very small, so the average reward is misleading.
In distributional reinforcement learning we have several predictors, which react differently to positive and negative errors.
Recently, similar distributions of dopamine cells was found in the brains of mice.

Computer Proofs

in

Mathematics

Universal deducer?

A universal deducer is a program which, given a mathematical statement, either proves it is true or proves it is false.
By results of Church, Gödel, Turing, such a program is impossible.
Practically, we can conclude that there is no best deducer, as any given proof can be found by some deducer but no deducer can find all proofs.

Some computer-assisted proofs

Four-colour problem: Any map can be coloured with at most $4$ colours.
Kepler Conjecture: The most efficient way to pack spheres is the hexagonal close packing.
Boolean Pythagorean triples problem: Is it possible to colour each of the positive integers either red or blue, so that no Pythagorean triple of integers $a$, $b$, $c$, satisfying $a^{2}+b^{2}=c^{2}$ are all the same color?
All these proofs are long (perhaps unavoidable).

Robbins conjecture

Robbins conjecture was a conjectural characterization of Boolean algebras in terms of associativity and commutativity of $\vee$ and the Robbins equation $\neg(\neg(a\vee b)\vee \neg(a \vee \neg b)) = a$.
This was conjectured in the 1930s, and finally proved in 1996 using the automated theorem prover EQP.
So far, this seems to be the only major success of deductive theorem provers.

A question on a blog of Terence Tao, asked to him by Apoorva Khare, was answered in PolyMath 14.
A crucial step in the discovery was a computer generated but human readable proof I posted.

Interactive Theorem Provers

Interactive Theorem Provers are software systems where proofs are obtained by human-machine collaboration.
The computer both finds (parts of) proofs and checks correctness.
Some very large mathematical proofs have been verified by such systems.
The ease of proving in such systems depends on how good it is at finding proofs.

Who guards the guards?

A computer verified proof is only as trustworthy as the system that verified the proof.
Following the de Bruijn principle, proofs are verified by a small trusted kernel, which can be thoroughly checked.
For example, the lean theorem prover has three (small) proof checkers written in three languages.

Foundations of mathematics

Foundations are rules for describing objects and statements and making deductions.
The standard foundations of mathematics are based on Set Theory and First-order logic.
However, formal proofs in these foundation become long and opaque.
Instead, interactive proof systems use richer foundations that have evolved over time.
A dramatic advance in the new foundations came about with the recent discovery of connections with topology, a branch of mathematics.

Formal methods

Mathematical proofs elsewhere

Formal methods

We specify and describe software, hardware etc. in precise mathematical terms.
We give mathematical proofs to ensure correct behavior.
This gives a much greater certainty of correctness.
However, proofs are much harder than tests.
Formal proofs use interactive theorem provers.

Do we need completely correct always?

	Pentium FDIV Bug	Fixing an error is very costly
	Therac 25 radiation machine	Safety critical
	WhatsApp Pegasus attack	A bug is a vulnerability

Users of formal methods

	Intel Chips	Fixing an error is very costly
	Paris driverless metro	Safety critical
	Scala dotty compiler	A bug is a vulnerability

The future of computer proofs?

Artificial Intelligence can:
- Make moves that we can appreciate.
- Judge value based on future rewards.
- Show originality.
- Acquire tacit (to us) knowledge.
- Work with limited and/or unstructured data, by self-play and by synthetic tasks.
- Organize observations naturally and efficiently, capturing global structure and enabling analogies.

Foundations give (efficient, modular) rules for generating objects, statements, proofs.
A reward can be defined in terms of power and efficiency of proving/disproving statements.
Mathematical heuristics can be captured with composite moves, and used for policy functions.
We can define reasonable value functions, e.g. recognizing non-trivial lemmas.
Behaviour cloning can use formalized mathematics, natural language processing.
Automating mathematics? It appears that there are clear approaches and no evident barriers.