Transcript The HOMER System for Discovery in Number Theory

The HOMER System for
Discovery in Number Theory
Simon Colton
Imperial College, London
Motivation

Newell and Simon:
– “Within 10 years (of 1957) a computer will discover
and prove an important mathematical theorem”

Alan Bundy:
– “His DReaM = Discovery and Reasoning in Maths”

Bob Kowalski:
– “It is more important to discover the most important
theorems than to prove unimportant ones”
An Overview of HOMER

Aim:
– To make conjectures in number theory

User supplies background knowledge:
– Number types: primes, squares, etc.
– Functions: tau, sigma, phi, etc.

HOMER makes conjectures about them
– Conjectures are meant to be interesting
– User is involved at certain stages
Otter, Maple, HR and the User
USER
OTTER
HOMER
MAPLE
Computer
Algebra System
First Order
Resolution Prover
HR
Automated Theory
Formation System
Roles of Individual Components

User: Provide Guidance
– Supply background information
– Verify/Falsify some conjectures produced

Maple: Generating Empirical Evidence
– Perform calculations

Otter: Increase Interestingness via Pruning
– Prove theorems from first principles

HR: Make Discoveries
– Invent concepts related to background
– Make conjectures relating concepts
Three Phases

Initialisation Phase
– User/Maple generate background info
• In a format suitable for HR

Discovery Cycle
– HR/Maple generate conjectures
• Using automated theory formation

Proving & Pruning Cycle
– User/Otter prove theorems
• HOMER discards any that Otter can prove
Initialisation Phase

User supplies:
– Maple code for concepts of interest
• Mathematicians don’t want to learn a language
– Integers to work with, e,g,. 1 – 250 & others

HOMER translates to HR’s input
– Calls Maple using the code and numbers
– Generates pairs of input/output
– Writes this in HR’s format
• Similar (in this case) to that for ILP systems
Example

Maple code:
isrefactorable_ := proc(num)
local output := false;
if (member(tau(num),divisors(num))=true) then output := true; fi;
output;
end:

HR input:
h01
isrefactorable_(n)
ascii:isrefactorable_(@n@)
isrefactorable_(1). isrefactorable_(2). isrefactorable_(8).
isrefactorable_(9). isrefactorable_(12). isrefactorable_(18).
Discovery Cycle:
1. Concept Formation

HR Forms concepts using production rules
– Restricted to 3 out of 10 in HOMER
– HR calls Maple again if it needs another calculation

Compose production rule
– Composes functions & predicates using conjunction
• Example1: tau(sigma(n)), Example2: odd primes

Split production rule
– Performs instantiation of variables to fixed constants
• Example: prime numbers (tau(n) = 2)

Exists production rule
– Introduces existential quantification
• Example: exists k s.t. tau(n) = k & sigma(n) = k,
Example Invention
Discovery Cycle:
2. Conjecture Making

Concepts are formed with
– Both a definition and a set of examples

Whenever a new concept is invented
 HR checks whether:
1. It has no examples
• Makes a non-existence conjecture
2. It has exactly same examples as another
• Makes an equivalence conjecture
3. The examples are subsumed by another
• Makes an implication conjecture
Example Conjecture

HR invents the concept of:
– Integers where number of divisors is prime

Later, it in invents the concept of:
– Integers where the sum of divisors is prime

Notices that the examples of latter
– Are all examples of the former

Makes the conjecture that
– isprime(sigma(n))  isprime(tau(n))
Proving and Pruning stage

The user can supply some axioms as
background knowledge, or nothing at all

Any conjecture the user proves
– Becomes an axiom of the theory

Anything Otter proves using the axioms
– Is discarded (hidden from the user)
– Because it will be “obviously” true to the user
Proving and Pruning Cycle
1. The User steps in

For each conjecture, the user is given
– The conjecture statement
– Up to two alternative conjectures
• From which the original follows

The user can choose to:
– Say the conjecture (or alternative) is true
– Supply a more general theorem
– Supply a counterexample to the conjecture
– Use HOMER to search for a counterexample
Proving and Pruning Cycle
2. Otter is employed

A set of axioms is built up
 Every new conjecture is passed to Otter
– Along with the axioms
– And ground instances of back. concepts
• E.g. isprime(2), tau(4)=3, sigma(5)=6, etc.

Any conjecture that Otter proves
–
–
–
–

Follows from the axioms (which user knows)
So it will be very easy for the user to prove it
And it won’t say much more than the axioms
So HOMER doesn’t show it to the user
After a while, Otter begins to prune many conjs
An Example (Pruned) Theorem

Tau(x) = number of divisors of x
 Sigma(x) = sum of divisors of x
 This conjecture looks interesting:
– isprime(n)  isodd(sigma(tau(n)))

But, this is actually really dull. Why?
 We know the axiom isprime(n)  tau(n)=2
– And ground instances: sigma(2)=3, isodd(3).

So, the conjecture is obviously true
 Otter proves this with no problem
– And so it is rightly discarded (user never sees it)
Design Considerations in HOMER

Background information given in a format
– Which is well known to users

Very few choices for users
– Mathematicians are notoriously uncomfortable
with mathematics software
• So, there are many defaults in HR and Otter which are set

Very simple user interface
– Asked questions they can’t ignore

Given the bare minimum of details
– Only the conjectures, nothing else
More Design Considerations

Absolute minimal number of dull results
– In PhD version of HR
• 90% of conjectures were dull
• Mostly tautologies (true regardless of semantics)

User can stop interacting at any time
– HOMER will continue to find results for them

Use of HTML format
– For improved presentation
Three Illustrative Results

Refactorable numbers
– (number of divisors is itself a divisor)
– Odd refactorables are squares
– HR’s results contributed to a maths paper

Prime sum of divisors implies prime
number of divisors
– “Level of an exercise at the end of a chapter”

Square numbers have odd sum of divisors
– Not as obvious as it might seem
A Session with
a Number Theorist

Sophie Huczynska (Math PostDoc)
– Completely new to HOMER

Session exploring totient function
– phi(n) = #integers less than and coprime to n
– Completely new to HOMER

Background information
– Integers: 1 to 50
– Functions: phi, sigma, tau
– Number types: odd, even, prime, square

~4 hours (including proving time)
– HOMER running for only a fraction of this
Session Results

Presented 59 out of thousands of conjs
– 38 have been subsequently proved,
– 4 were shown to be false
– 17 remain open

Interestingness
– None were tautologies
– 7 followed trivially from definitions (mostly at start)
– Difficulty decreased as session continued
• 2 out of first 30 settled
• 8 out of final 10 still open
– Four which are “number theoretically interesting”
Two “Number Theoretically
Interesting” Results
(a) phi(n) is odd  phi(n) = 1
 (b) phi(n) = 1  n=1 or n=2
 Combined to give:

– phi(n) is even  n > 2 [is this obvious?]

phi(n) is square  tau(n) is even
– Described as “cute”
– Proof required theorem viewed correctly
• i.e., by considering the contrapositive
An Evaluation of Potential

Sophie’s Evaluation
– After more testing with HOMER

Not ready yet for research mathematics
– Limited nature of the background concepts
• Nothing likely to surprise the user
– Complication in theorems is not a good thing
• Prefer simpler results about complicated functions

Potential Applications
– Recreational Mathematics
• User invents something new, HOMER performs exploration
– Setting of tutorial questions
• To give students a feel for number theoretic functions
Recommendations for
Future Versions

Combine with NumbersWithNames
– Program which uses Encyclopedia of integer
sequences to make conjectures
• Problem: flat file (sequences cannot be extended)
– Would possibly make surprising conjectures

Allow user defined production rules (PRs)
– Which are more domain specific
• (HR’s PRs work just as well in bioinformatics…)
– E.g., Dirichlet convolution
• Implemented yesterday!
A Demonstration…

Re-invention of Refactorable Results
– A number is refactorable if the number of divisors
is itself a divisor
– Re-invented by HR in 1998 (original 1990)
– 1, 2, 8, 9,…

Also: Anti-tau numbers
– Invented by Josh Zelinsky
• High school student inspired by refactorables
– They are coprime with the number of divisors
– 1, 3, 4, 5, 7, 11,…