## What does it do?

It checks your proofs. Suppose you have a potential proof of X and you want to be sure that your proof is correct. X might be a statement of mathematics, philosophy, theology, etc. You just have to write your proof in the language of Oak, and then Oak will tell you whether or not it is correct.

## What doesn't it do?

It doesn't write the proof for you. Rather, it gives you a formal language in which to write a proof, and then checks that the proof is correct.

## How does it work?

Oak translates each step of your proof into a statement of first-order logic, and passes it to an external theorem prover called

E. The prover then checks whether the given statement is valid. If it is, Oak proceeds to the next step of your proof. If it isn't, or if the prover exceeds a certain "amount of work", Oak stops and tells you there was a problem.

## What does it look like?

Here is a simple example of a proof written in the language of Oak.

**axiom** **every** man **is** mortal
**axiom** Socrates **is**** ****a** man
**so** Socrates **is** mortal

Here is a more complicated example. This proof and its dependencies are available in Oak's examples directory.
Primes **is** infinite
**proof**
**suppose** 1: Primes **is** finite # to obtain a contradiction
2: **for**** ****some** p **in** N, p = product[Primes] **by** 1,product_set_in_N
3: **for**** ****some** q **in** N, q = p+1
4: **for**** ****some** d **in** N, d divides q **and** d **is** prime
**proof**
**for**** ****all** n **in** Primes, n > 0
**by** primes_def,prime_def,nonnegative,total_order
**so** p > 0 **by** product_set_positive,1,2
**so** q > 1 **by** 3,ineq_def,add_commute
**so** **thesis** **by** prime_factor
**end**
d divides p **by** divides_product,primes_def,1,2,4
**so** d divides 1 **by** divides_diff,3,4
**so** d **is** **not** prime **by** prime_def,divides_one,total_order
**so** **contradiction** **by** 4
**end**
**so** **thesis** **by** infinite_def
**end**

## Who made it?

Oak was created by

Tim Smith.