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. |
| ctmu.oak | Chris Langan's Cognitive-Theoretic Model of the Universe (CTMU). |
| 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. |