Oak Examples

Oak in action.

Here are some examples of Oak proofs. You can download them as a zip file here.

If you would like to contribute to the examples, you can do so via Oak's page at GitHub.

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.
descartes.oakProofs from Descartes' Meditations on First Philosophy.
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.
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 elements of a set.
set.oakAxioms and results for sets.
square_root_two.oakA proof from first principles that √2 is irrational.