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 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.