Transcript Calculation Invention and Deduction

Calculation Invention and Deduction
Dr. Simon Colton
Imperial College London
(Formerly at Edinburgh)
YVR in Karlsruhe & Saarbrucken
A Plausible Model for
Mathematical Discover
1. Do some calculations 2. Notice a pattern
Computer Algebra
Machine Learning
3. Prove pattern is true
Automated Theorem
Proving
Calculation
Invention
Deduction
MAPLE
HR
OTTER
A Nice Example
1926 Hungarian Mathematics Competition:
n(n+1)(n+2)(n+3) is never a square number
Plug and Chug
[Calculate]
1*2*3*4 = 24, 2*3*4*5 = 120, 3*4*5*6 = 360
Eureka!
[Invent]
20 = 25-1 = 5*5-1, 120=11*11-1, 360 = 19*19-1
Numbers are all squares – 1
Therefore
[Deduce]
They cannot be square numbers
The HR System
Performs automated theory formation
Start with axioms (or some background)
End with examples, concepts, conjectures, theorems
Cycle of mathematical activity
Invents new concepts based on old ones
Makes conjectures empirically about the concepts
Tries to prove the conjectures using a theorem
prover or disprove them using a model generator
Works in number theory, graph theory, various algebras
One of a few programs to add to mathematics
Calculemus Project 1
Adding to a Library of Theorems
Work done with Jürgen Zimmer (Saarbrucken) and Geoff Sutcliffe (Miami)
I learned about the Mathweb software bus (task 2.1)
TPTP library of mathematical theorems
To help see who has the best theorem prover
Want to differentiate, not beat provers
HR within MathWeb testing three provers
Found 12,000 theorems in one session
Each prover was beaten by a theorem others could prove
Now added 184 theorems to the library
Only non-human to add to the library
Calculemus Project 2
Discriminant Discovery
Work done with Andreas Meier (Saarbrucken) & Volker Sorge (Birmingham)
I learned about proof planning and omega (task 2.3)
What’s the difference between these algebras?
Idempotent element appearing only once on the diagonal
Found by HR as a discriminant in the general case
Part of a larger project to classify residue classes
Using proof planning in Omega, and many other systems
HR found a discriminant for 97% of the 817 pairs given to it
Calculemus Project 3
The HOMER System
Work done with Jacques Calmet and Clemens
Ballarin at Karlsruhe (task 2.2)
I learned about about Maple (computer algebra system)
Aimed at (recreational) number theorists
HR is given some Maple input (computer algebra)
Makes conjectures about the functions supplied
Uses Otter to prove them
Throws away any which Otter can prove
Because they are unlikely to be interesting to user
Some Results from HOMER
Only non-human to add to
Encyclopedia of integer sequences (80,000+)
Assessed by mathematician (never seen HOMER)
A session in an afternoon produced 59 conjs
38 proved, 4 false, 17 open
Four were “number theoretically interesting”
Nice results:
Sum of divisors of squares is odd
Phi(n) is square implies Tau(n) is even
Perfect numbers are pernicious