Automating Mathematics?
Siddhartha Gadgil
Department of Mathematics
Indian Institute of Science
Bangalore
 |
 |
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?
- 2
- 3
- 4
- 5
- 6
- 7
- 8
- 9
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 88
- 89
- 90
- 91
- 92
- 93
- 94
- 95
- 96
- 97
- 98
- 99
- 100
- 401
- 402
- 403
- 404
- 405
- 406
- 407
- 408
- 409
- 410
- 411
- 412
- 413
- 414
- 415
- 416
- 417
- 418
- 419
- 420
- 421
- 422
- 423
- 424
- 425
- 426
- 427
- 428
- 429
- 430
- 431
- 432
- 433
- 434
- 435
- 436
- 437
- 438
- 439
- 440
- 441
- 442
- 443
- 444
- 445
- 446
- 447
- 448
- 449
- 450
- 451
- 452
- 453
- 454
- 455
- 456
- 457
- 458
- 459
- 460
- 461
- 462
- 463
- 464
- 465
- 466
- 467
- 468
- 469
- 470
- 471
- 472
- 473
- 474
- 475
- 476
- 477
- 478
- 479
- 480
- 481
- 482
- 483
- 484
- 485
- 486
- 487
- 488
- 489
- 490
- 491
- 492
- 493
- 494
- 495
- 496
- 497
- 498
- 499
- 500
- 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?
- 2
- 3
- 4
- 5
- 6
- 7
- 8
- 9
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 88
- 89
- 90
- 91
- 92
- 93
- 94
- 95
- 96
- 97
- 98
- 99
- 100
- 401
- 402
- 403
- 404
- 405
- 406
- 407
- 408
- 409
- 410
- 411
- 412
- 413
- 414
- 415
- 416
- 417
- 418
- 419
- 420
- 421
- 422
- 423
- 424
- 425
- 426
- 427
- 428
- 429
- 430
- 431
- 432
- 433
- 434
- 435
- 436
- 437
- 438
- 439
- 440
- 441
- 442
- 443
- 444
- 445
- 446
- 447
- 448
- 449
- 450
- 451
- 452
- 453
- 454
- 455
- 456
- 457
- 458
- 459
- 460
- 461
- 462
- 463
- 464
- 465
- 466
- 467
- 468
- 469
- 470
- 471
- 472
- 473
- 474
- 475
- 476
- 477
- 478
- 479
- 480
- 481
- 482
- 483
- 484
- 485
- 486
- 487
- 488
- 489
- 490
- 491
- 492
- 493
- 494
- 495
- 496
- 497
- 498
- 499
- 500
- 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$:
- 3
- 5
- 7
- 3
- 7
- 11
- 3
- 11
- 19
- 3
- 13
- 23
- 3
- 17
- 31
- 3
- 23
- 43
- 3
- 31
- 59
- 3
- 37
- 71
- 3
- 41
- 79
- 3
- 43
- 83
- 3
- 53
- 103
- 5
- 29
- 53
- 7
- 13
- 19
- 7
- 43
- 79
- 11
- 29
- 47
- 11
- 47
- 83
- 11
- 59
- 107
- 13
- 37
- 61
- 17
- 23
- 29
- 17
- 53
- 89
- 17
- 59
- 101
- 19
- 31
- 43
- 19
- 43
- 67
- 19
- 61
- 103
- 23
- 41
- 59
- 23
- 47
- 71
- 29
- 41
- 53
- 29
- 59
- 89
- 31
- 37
- 43
- 47
- 53
- 59
- There are $110386$ of these among the first million.
-
Some prime arithmetic progressions of length $4$:
- 5
- 23
- 41
- 59
- 5
- 59
- 113
- 167
- 5
- 89
- 173
- 257
- 7
- 19
- 31
- 43
- 7
- 79
- 151
- 223
- 11
- 17
- 23
- 29
- 13
- 43
- 73
- 103
- 13
- 61
- 109
- 157
- 17
- 29
- 41
- 53
- 19
- 73
- 127
- 181
- 19
- 79
- 139
- 199
- 23
- 53
- 83
- 113
- 29
- 83
- 137
- 191
- 31
- 67
- 103
- 139
- 41
- 47
- 53
- 59
- 41
- 71
- 101
- 131
- 43
- 61
- 79
- 97
- 47
- 59
- 71
- 83
- 47
- 89
- 131
- 173
- 53
- 71
- 89
- 107
- 59
- 83
- 107
- 131
- 61
- 67
- 73
- 79
- There are $27836$ of these among the first million.
-
Some prime arithmetic progressions of length $5$:
- 5
- 11
- 17
- 23
- 29
- 5
- 17
- 29
- 41
- 53
- 5
- 47
- 89
- 131
- 173
- 5
- 53
- 101
- 149
- 197
- 5
- 101
- 197
- 293
- 389
- 5
- 131
- 257
- 383
- 509
- 11
- 41
- 71
- 101
- 131
- 13
- 163
- 313
- 463
- 613
- 17
- 167
- 317
- 467
- 617
- 29
- 149
- 269
- 389
- 509
- 37
- 67
- 97
- 127
- 157
- 43
- 103
- 163
- 223
- 283
- 61
- 151
- 241
- 331
- 421
- 71
- 131
- 191
- 251
- 311
- 83
- 173
- 263
- 353
- 443
- 89
- 179
- 269
- 359
- 449
- 113
- 173
- 233
- 293
- 353
- 137
- 167
- 197
- 227
- 257
- There are $3665$ of these among the first million.
-
Some prime arithmetic progressions of length $6$:
- 7
- 37
- 67
- 97
- 127
- 157
- 11
- 71
- 131
- 191
- 251
- 311
- 13
- 103
- 193
- 283
- 373
- 463
- 13
- 223
- 433
- 643
- 853
- 1063
- 23
- 263
- 503
- 743
- 983
- 1223
- 41
- 461
- 881
- 1301
- 1721
- 2141
- 53
- 113
- 173
- 233
- 293
- 353
- 73
- 223
- 373
- 523
- 673
- 823
- 83
- 383
- 683
- 983
- 1283
- 1583
- 107
- 137
- 167
- 197
- 227
- 257
- 127
- 457
- 787
- 1117
- 1447
- 1777
- 157
- 307
- 457
- 607
- 757
- 907
- 239
- 359
- 479
- 599
- 719
- 839
- 281
- 401
- 521
- 641
- 761
- 881
- 359
- 389
- 419
- 449
- 479
- 509
- There are $980$ of these among the first million.
-
Some prime arithmetic progressions of length $7$:
- 7
- 157
- 307
- 457
- 607
- 757
- 907
- 47
- 257
- 467
- 677
- 887
- 1097
- 1307
- 53
- 1103
- 2153
- 3203
- 4253
- 5303
- 6353
- 71
- 2381
- 4691
- 7001
- 9311
- 11621
- 13931
- 179
- 389
- 599
- 809
- 1019
- 1229
- 1439
- 193
- 613
- 1033
- 1453
- 1873
- 2293
- 2713
- 359
- 1619
- 2879
- 4139
- 5399
- 6659
- 7919
- 829
- 1039
- 1249
- 1459
- 1669
- 1879
- 2089
- 1061
- 1901
- 2741
- 3581
- 4421
- 5261
- 6101
- 1091
- 1301
- 1511
- 1721
- 1931
- 2141
- 2351
- 1453
- 1663
- 1873
- 2083
- 2293
- 2503
- 2713
- There are $127$ of these among the first million.
-
Some prime arithmetic progressions of length $8$:
- 619
- 829
- 1039
- 1249
- 1459
- 1669
- 1879
- 2089
- 881
- 1091
- 1301
- 1511
- 1721
- 1931
- 2141
- 2351
- 1019
- 3329
- 5639
- 7949
- 10259
- 12569
- 14879
- 17189
- 1091
- 3821
- 6551
- 9281
- 12011
- 14741
- 17471
- 20201
- 1289
- 2969
- 4649
- 6329
- 8009
- 9689
- 11369
- 13049
- 1637
- 2267
- 2897
- 3527
- 4157
- 4787
- 5417
- 6047
- 1847
- 3947
- 6047
- 8147
- 10247
- 12347
- 14447
- 16547
- 2239
- 2659
- 3079
- 3499
- 3919
- 4339
- 4759
- 5179
- 2693
- 4583
- 6473
- 8363
- 10253
- 12143
- 14033
- 15923
- 3323
- 4583
- 5843
- 7103
- 8363
- 9623
- 10883
- 12143
- There are $46$ of these among the first million.
- 17
- 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.
- 199
- 409
- 619
- 829
- 1039
- 1249
- 1459
- 1669
- 1879
- 2089
- 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
- 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.
Automating Mathematics?
Siddhartha Gadgil
Department of Mathematics
Indian Institute of Science
Bangalore
http://math.iisc.ac.in/~gadgil/
https://github.com/siddhartha-gadgil/ProvingGround