Tag: Isar

• Probabilistic reasoning and formal proof (21 Aug 2024)
  
• A tricky lower bound proof (08 Aug 2024)
  
• Small examples involving binomial coefficients (22 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)
  
• Automation and engineering in mathematics, by Pedro Sánchez Terraf (16 Nov 2022)
  
• Ackermann's function is not primitive recursive, II (07 Sep 2022)
  
• Ackermann's function is not primitive recursive, I (31 Aug 2022)
  
• Formalising Gödel's incompleteness theorems, II: Σ-formulas (25 May 2022)
  
• A classical proof: exponentials are irrational (16 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)