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.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. |
| 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, published in 1666. |
| 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 sets. |
| set.oak | Axioms and results for sets. |
| square_root_two.oak | A proof from first principles that √2 is irrational. |