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
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 by nat_closed_add
4: for some d in N, d divides q and d is prime
for all n in Primes, n > 0
so p > 0 by product_set_positive,1,2
so q > 1 by 3,ineq_def,add_commute,total_order
so thesis by prime_factor
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
so thesis by infinite_def
Who made it?
Oak was created by Tim Smith