Oak

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 can be found on Oak's examples page.

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.