# Tag: examples

- Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel (08 Nov 2023)

- Small examples involving binomial coefficients (22 Mar 2023)

- The semantics of a simple functional language (08 Mar 2023)

- Verifying the binary algorithm for greatest common divisors (22 Feb 2023)

- An irrationality proof involving cube roots (08 Feb 2023)

- Formalising a new proof that the square root of two is irrational (18 Jan 2023)

- Martin-Löf type theory in Isabelle: examples (30 Nov 2022)

- Proving termination with multiset orderings (26 Oct 2022)

- Ackermann's function is not primitive recursive, II (07 Sep 2022)

- Ackermann's function is not primitive recursive, I (31 Aug 2022)

- A few small formalisation challenges (03 Aug 2022)

- Dealing with descriptions in Isabelle/HOL: least, greatest, whatever (08 Jun 2022)

- Getting started with Isabelle: baby examples, cool proof methods (04 May 2022)

- The quaternions—and type classes (09 Mar 2022)

- A classical proof: exponentials are irrational (16 Feb 2022)

- Fun with Ackermann's function (09 Feb 2022)

- Readability in proofs: the mean value theorem (22 Dec 2021)

- An Experiment: the Cauchy–Schwarz inequality (17 Nov 2021)

- More on Fibonacci numbers, with equational reasoning (20 Oct 2021)

- Introductory example: Fibonacci numbers (13 Oct 2021)