RECOGNITION AND COMPUTATION OF MATHEMATICAL PROOFS BY INDUCTION

Connor Flood, 2015

W|A Math Content Developer
University of Waterloo Graduate Student (MMath - Computer Science)
connorf@wolfram.com

Join the Conversation #WolframTechConf

Proof by Principle of Mathematical Induction (PMI)

Background

Logical proof of a given query

Domino effect

Introduced ~1st year university

({{Ex : Prove 2 n+7<(((n+7))^2), for n≥1 

Step 1) Base Case (show true for n = 1) 

Step 2) Inductive Step (show true for n = k+1, assuming true for k), 
}})

Recipe Book

Proofs = Recipes

A program can perform proofs only on what it is “prepared” for

No universal pattern

Constantly improving its breadth of capabilities

Nearly impossible to include a full solution to EVERY possible provable query

Distinguish between general and specific cases

Supported Queries

Summation/Product Equalities

Prove (∑_(i=1)^n)(2^i)==(2^(n+1))-2, for n≥1

Expression Divisibility

Prove (8^n)-(3^n) is divisible by 5, for n≥1

Expression Inequalities

Prove 2 n+7<(((n+7))^2), for n≥1

First Stage

Object-Oriented Programming Approach (Java)

Wolfram Alpha APIs

Why APIs?

Original purpose was only for simplifying expressions

Made calls to Alpha for all calculations

Easy to use

Converted output of pods into Strings

Program Results

Did not show any textual steps

Very limited in queries

User input was not ideal

API calls were time consuming

First Stage Demonstration

Mathematica Saves the Day

Functional Language Programming Approach

Required much less code

Showed greater accuracy and easability in terms of scalability

Pattern Matching

One of the biggest benefits

Pattern matching in Java was a huge limitation

Can easily verify the type of input expressions

Further Breakdown Query Types

Solidifying Proof Types

Recipe book

Can still be added to and improved upon

More than 1 way to complete a proof using PMI

General vs Specific scale results in proof types being combined or isolated

Types of Return Results

Logic map for query results

Scope Query Domain

Take difference in LHS and RHS

Prove 2 n+7 +sin(n)<(((n+7))^2) + sin(n), for n≥1

Add constant

Prove 5n + 8 < (2^n), for n≥1

Base Case Pass -> Inductive Step Fails

Prove 4n+7 >(2^n), for n≥4

All horses are the same color

Prove 4n<(2^n), for n≥0

What Next?

Further exploration

Increase coverage for induction (series)

Explore other types of proofs (contradiction, existence)

Research if/how machine learning could play a role

RECOGNITION AND COMPUTATION OF MATHEMATICAL PROOFS BY INDUCTION

Connor Flood, 2015

W|A Math Content Developer
University of Waterloo Graduate Student (MMath - Computer Science)
connorf@wolfram.com

Join the Conversation #WolframTechConf