Tag: examples

• Probabilistic reasoning and formal proof (21 Aug 2024)
  
• A tricky lower bound proof (08 Aug 2024)
  
• Two small examples by Fields medallists (28 Feb 2024)
  
• 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)