The Curious Engineer

All blogs / Math

Machine Logic

lawrencecpaulson.github.io

Machine Logic is Lawrence Paulson's blog on Isabelle/HOL and related topics.

MathFunctional / PL theory

’21’22’23’24’25’26
Posts
115 from 9 Aug 2021 to 30 Oct 2026
Posting
monthly (14 in the last year)
Kind
personal blog
Feed
https://lawrencecpaulson.github.io/feed.xml

2026 11

  1. Tim Smiley: an anecdote
  2. A Summer with Claude and Relative Arbitrage, by Dmitriy Traytel
  3. Plagiarism in the age of AI
  4. How I came to write THAT paper with Leslie Lamport
  5. Why is it all in the kernel?
  6. The Dottie number
  7. Nullius in verba: the motto of the Royal Society
  8. Mizar: the first usable proof assistant for mathematics
  9. "Why not just use Lean?"
  10. Memories: doing my PhD at Stanford, under John L Hennessy
  11. Broken proofs and broken provers

2025 16

  1. 50 years of proof assistants
  2. Set theory with types
  3. "Why don't you use dependent types?"
  4. Most proofs are trivial
  5. Everything you know is wrong
  6. earlier post
  7. Definite integrals, II: improper integrals
  8. Last time
  9. Finish your degree!
  10. Inductive definitions
  11. previous post
  12. The philosophical problem of induction, and the problem of Fetzer
  13. A trickier lower bound proof
  14. Revisiting an early critique of formal verification
  15. Formalising an easy proof: Dirichlet's approximation theorem
  16. Computing huge Fibonacci numbers, by proof and by code

2024 10

  1. For the holidays, some problems about prime divisors
  2. Isabelle quick start guide
  3. The λ-calculus, 2: the Church-Rosser theorem
  4. Introduction to the λ-calculus
  5. Probabilistic reasoning and formal proof
  6. That post
  7. previous post
  8. Two small examples by Fields medallists
  9. Contradictions and the Principle of Explosion
  10. last time

2023 18

  1. Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel
  2. What do we mean by "the foundations of mathematics"?
  3. The concept of proof within the context of machine mathematics
  4. The End (?) of the ALEXANDRIA project
  5. Propositions as types: explained (and debunked)
  6. When is a computer proof a proof?
  7. Hao Wang on the formalisation of mathematics
  8. Porting the HOL Light metric space library
  9. The ALEXANDRIA Project: what has been accomplished?
  10. wildly overrated philosopher
  11. Small examples involving binomial coefficients
  12. The semantics of a simple functional language
  13. Verifying the binary algorithm for greatest common divisors
  14. An irrationality proof involving cube roots
  15. On the infinite
  16. formalised a new proof
  17. Memories: artificial intelligence at Stanford in the 70s
  18. Mike Gordon and hardware verification

2022 47

  1. MetiTarski: an automatic prover for real-valued special functions
  2. Thoughts on user interfaces for theorem provers
  3. Memories: first exposure to computers
  4. Martin-Löf type theory in Isabelle: examples
  5. previous post
  6. Automation and engineering in mathematics, by Pedro Sánchez Terraf
  7. (Hilbert, Isabelle) and more universal pairs, by Marco David
  8. Verifying cryptographic protocols, II: a simple example
  9. Proving termination with multiset orderings
  10. Not long ago
  11. Verifying distributed systems with Isabelle/HOL, by Martin Kleppmann
  12. Memories: Edinburgh ML to Standard ML
  13. Memories: Edinburgh LCF, Cambridge LCF, HOL88
  14. Porting libraries of mathematics between proof assistants
  15. Ackermann's function is not primitive recursive, II
  16. previous post
  17. BDDs in HOL: the coolest thing Mike Gordon ever did
  18. The formalisation of nonstandard analysis
  19. A few small formalisation challenges
  20. models and the real world
  21. I described
  22. On Turing machines
  23. What is the point of formalising mathematics?
  24. Formalising Ramsey theory, II
  25. Dealing with descriptions in Isabelle/HOL: least, greatest, whatever
  26. Formalising Gödel's incompleteness theorems, III: Coding and Bound Variables
  27. Formalising Gödel's incompleteness theorems, II: Σ-formulas
  28. Formalising Gödel's incompleteness theorems, I
  29. Getting started: basic Isabelle/jEdit tricks
  30. previous post
  31. Wetzel's problem and the continuum hypothesis
  32. Why are you being constructive?
  33. sledgehammer
  34. Integrating Zermelo-Fraenkel set theory with higher-order logic
  35. Equivalence classes and quotienting
  36. Type classes versus locales
  37. choice between set theory and type theory
  38. quaternions
  39. previous post
  40. previous post
  41. A classical proof: exponentials are irrational
  42. earlier post
  43. Wang had built an automatic theorem prover
  44. Is Zermelo-Fraenkel set theory the foundation of mathematics?
  45. Formalising extremal graph theory, I
  46. Proving the obvious
  47. earlier post

2021 13

  1. previous post
  2. Readability in proofs: the mean value theorem
  3. Do Gödel's incompleteness theorems matter?
  4. ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician
  5. Undefined values, or what do we get when we divide by zero?
  6. Intuitionism and constructive logic
  7. An Experiment: the Cauchy–Schwarz inequality
  8. The axiom of choice and descriptions
  9. AUTOMATH
  10. previously considered
  11. More on Fibonacci numbers, with equational reasoning
  12. previous post
  13. Welcome to Machine Logic!