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.oak | Proof 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.oak | Comprehension axioms, for properties and operations. |
descartes.oak | Proofs from Descartes' Meditations on First Philosophy. |
godel_disjunction.oak | Gödel's disjunction about minds and machines. |
graph.oak | Definitions and results for graphs. |
infinite_primes.oak | Definitions and results for divisibility and prime numbers, culminating in a proof that the set of primes is infinite. |
kalam.oak | Kalam cosmological argument. |
konigsberg.oak | Euler's result that no path crosses each of the bridges of Königsberg once and only once. |
leibniz.oak | A formalization of Leibniz's proof of the existence of God in his Dissertatio de Arte Combinatoria. |
list.oak | Axioms and results for lists, including linked lists. |
naturals.oak | Axioms and results for natural numbers. |
product.oak | Recursive definition of the product of a finite set of natural numbers. |
recursion.oak | A recursion theorem for functions from natural numbers to elements of a set. |
set.oak | Axioms and results for sets. |
square_root_two.oak | A proof from first principles that √2 is irrational. |