Oak Examples

Oak in action.

Here are some examples of Oak proofs. They are also available in Oak's GitHub repository, as well as in the prepackaged downloads on the main page.

bernstein.oakProof of the Bernstein theorem that if there is an injection from A to B and an injection from B to A, then there is a bijection between A and B.
comprehension.oakComprehension axioms, for properties and operations.
godel_disjunction.oakGödel's disjunction about minds and machines.
graph.oakDefinitions and results for graphs.
infinite_primes.oakDefinitions and results for divisibility and prime numbers, culminating in a proof that the set of primes is infinite.
kalam.oakKalam cosmological argument.
konigsberg.oakEuler's result that no path crosses each of the bridges of Königsberg once and only once.
leibniz.oakA formalization of Leibniz's proof of the existence of God in his Dissertatio de Arte Combinatoria, published in 1666.
list.oakAxioms and results for lists, including linked lists.
naturals.oakAxioms and results for natural numbers.
product.oakRecursive definition of the product of a finite set of natural numbers.
recursion.oakA recursion theorem for functions from natural numbers to sets.
set.oakAxioms and results for sets.
square_root_two.oakA proof from first principles that √2 is irrational.