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. |