# 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)