Tag: Isabelle

• The mysteries and frustrations of numerical proofs (25 Jul 2024)
  
• Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel (08 Nov 2023)
  
• The End (?) of the ALEXANDRIA project (31 Aug 2023)
  
• Porting the HOL Light metric space library (12 Jul 2023)
  
• The ALEXANDRIA Project: what has been accomplished? (27 Apr 2023)
  
• Martin-Löf type theory in Isabelle: examples (30 Nov 2022)
  
• Martin-Löf type theory in Isabelle: formalisation (23 Nov 2022)
  
• (Hilbert, Isabelle) and more universal pairs, by Marco David (09 Nov 2022)
  
• Porting libraries of mathematics between proof assistants (14 Sep 2022)
  
• How Isabelle emerged from the trends of the 1980s (13 Jul 2022)
  
• Formalising Ramsey theory, II (15 Jun 2022)
  
• Dealing with descriptions in Isabelle/HOL: least, greatest, whatever (08 Jun 2022)
  
• Getting started: basic Isabelle/jEdit tricks (11 May 2022)
  
• Getting started with Isabelle: baby examples, cool proof methods (04 May 2022)
  
• Type classes versus locales (23 Mar 2022)
  
• Axiomatic type classes: some history, some examples (02 Mar 2022)
  
• A classical proof: exponentials are irrational (16 Feb 2022)
  
• Fun with Ackermann's function (09 Feb 2022)
  
• ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (08 Dec 2021)
  
• Introductory example: Fibonacci numbers (13 Oct 2021)