Top all-time · #1815
Lawrence Paulson
Personal blog · lawrencecpaulson.github.iomathprogramming
Lawrence Paulson writes Machine Logic, a personal blog at lawrencecpaulson.github.io about math and programming. Since 2022, 40 different Hacker News readers have linked it 70 times, most often “Why is it all in the kernel?”. It is still writing: the last post was on 2026-10-30, and you can follow it by feed.
Too few sampled comments (13) to say how often HN recommends it.?
Why HN links it
HN readers link Lawrence Paulson's Machine Logic blog for posts on formal logic and theorem provers such as Isabelle, including the Collatz post on what belongs in a proof kernel and the division-by-zero post.
Summarised by Claude from a sample of 13 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Most-linked posts?
- Why is it all in the kernel?3 people · 3 mentions · first linked 2026-08-03
- /2022/01/05/LCF.html2 people · 2 mentions · first linked 2022-09-10
- Memories: Doing my PhD at Stanford, under John L Hennessy2 people · 2 mentions · first linked 2026-02-13
- 50 Years of Proof Assistants2 people · 2 mentions · first linked 2025-12-13
- Program verification is not all-or-nothing2 people · 2 mentions · first linked 2025-09-11
- "Why not just use Lean?"2 people · 2 mentions · first linked 2026-04-23
- Types versus sets (and what about categories?)2 people · 2 mentions · first linked 2022-03-16
- Mizar: The first usable proof assistant for mathematics2 people · 2 mentions · first linked 2026-05-07
- Set theory with types2 people · 2 mentions · first linked 2025-11-21
- Propositions as Types: Explained (and Debunked)2 people · 2 mentions · first linked 2024-01-06
What Hacker News says?
the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-... ...and for those who are looking to roll-their-own: https://ammkrn.github.io/type_checking_in_lean4/title_page.h... ...and some thoughts on putting stuff in the kernel: https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
Comment linking /2026/07/30/Collatz.html
on “Formalizing Fermat's Last Theorem”Submitted Why don't you use dependent types? as a story · 269 points
HN discussionIt doesn't have to be the statement, see the recent incident where someone used an LLM to generate a lean refutation of the collatz conjecture, the lean proof exploited bugs in the lean kernel. https://lawrencecpaulson.github.io/2026/07/30/Collatz.html
Comment linking /2026/07/30/Collatz.html
on “OpenAI withdraws three mathematical results”Submitted Verifying distributed systems with Isabelle/HOL as a story · 163 points
HN discussionYou have conveniently skipped the "Philosophical Objections" section in Wikipedia which i had pointed out and which would have given you some hints as to what i am saying. > A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm ... I think this is really a disagreement on phraseology though, nothing deeper. It is mathematical in nature but if the…
Comment linking /2023/08/09/computer_proof.html
on “Mathematics for Computer Science (2024)”Submitted 50 years of proof assistants as a story · 142 points
HN discussionA random walk can do mathematics, with this kind of infrastructure. Isabelle/HOL has a tool called Sledgehammer, which is the hackiest hack that ever hacked[0], basically amounting to "run a load of provers in parallel, with as much munging as it takes". (Plumbing them together is a serious research contribution, which I'm not at all belittling.) I've yet to see ChatGPT achieve anything like what it's capable of. [0…
Comment linking /2022/04/13/Sledgehammer.html
on “Mathematical exploration and discovery at scale”Submitted Set theory with types as a story · 125 points
HN discussion> Formally proving with a system based on probabilities (temperature, etc.) is for me an oxymoron. But I am not a mathematician. In the context of automated theorem proving, proof search and proof checking could not be more different. Proof search is undecidable for most logics. For that reason, heuristics are commonly used to guide proof search. This has always been the case; heuristic proof search predates the use…
Comment linking /2022/01/05/LCF.html
on “DeepSeek: Advancing theorem proving in LLMs through large-scale synthetic data”Submitted Memories: Edinburgh ML to Standard ML as a story · 119 points
HN discussionAnother aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why…
Comment linking /2024/02/28/Gowers_bijection_example.html
on “The Fermat's Last Theorem Project”Submitted Formalising Gödel's incompleteness theorems, I as a story · 83 points
HN discussionYes I wholeheartedly agree, rust is definitely overpromising in that department. The language has grown too large too quickly imho, and having the compiler as a formally verifying aide when the foundations/axioms aren't defined yet certainly leaves a bad aftertaste for me. In a sense rust hasn't managed to reach it's de Bruijn criterion yet, see https://lawrencecpaulson.github.io/2022/01/05/LCF.html However, the ver…
Comment linking /2022/01/05/LCF.html
on “Zig VP of community comments on Rust”Submitted Types versus sets (and what about categories?) as a story · 79 points
HN discussionGreat article, two minor nitpicks: > To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes. This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice…
Comment linking /2023/08/23/Propositions_as_Types.html
on “Types of Types: Common to Exotic”Submitted Introduction to the λ-Calculus as a story · 46 points
HN discussionWell, at some point you have to define what you mean by "proof by contradiction". I was responding to your statement, "prove something by showing that the alternative is unsound". You can prove that something is false that way without needing classical logic. Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathli…
Comment linking /2021/11/24/Intuitionism.html
on “"Why not just use Lean?"”Submitted On Turing Machines as a story · 26 points
HN discussionAlso, see: Memories: Edinburgh ML to Standard ML at https://lawrencecpaulson.github.io//2022/10/05/Standard_ML.h...
Comment linking //2022/10/05/Standard_ML.html
on “History of Standard ML [pdf]”Submitted "Why not just use Lean?" as a story · 13 points
HN discussionThere's the classic "Believing the Axioms" by Penelope Maddy [0] [1], the excellent study guide "Teach Yourself Logic" [2], plenty of great articles on the Stanford Encyclopedia of Philosophy (e.g. [3] or [4]), Dana Scott's "Lambda Calculus: Some Models, Some Philosophy" [5], and too many other interesting rabbit holes to count (i.e. resolution, unification, cut elimination, nonstandard models of arithmetic...) [0]…
Comment linking /papers/Scott-Models.pdf
on “Ask HN: Introductory reading on philosophy of mathematics/formal logic?”Submitted Mike Gordon and hardware verification (2023) as a story · 12 points
HN discussion(Original title shortened because it's too long.) Why higher-order logic is a good formalisation for specifying and verifying hardware Mike Gordon September 1985, 28 pages DOI https://doi.org/10.48456/tr-77 Abstract Higher order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language, and 2. a formalism for proving that designs m…
Comment linking /2023/01/04/Hardware_Verification.html
on “Why higher-order logic is a good formalisation for hardware”Submitted Memories: Edinburgh ML to Standard ML as a story · 8 points
HN discussionThe standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out. https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://www.hillelwayne.com/post/divide-by-zero/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... You'll need to do some thinking/proof to find out if it works for you.
Comment linking /2021/12/01/Undefined.html
on “Why is division so much more complex than other arithmetic operations?”Submitted Formalising a new proof that the square root of two is irrational as a story · 7 points
HN discussionSubmitted Set Theory with Types as a story · 6 points
HN discussionSubmitted Types versus sets (and what about categories?) as a story · 6 points
HN discussionSubmitted Everything you know is wrong as a story · 5 points
HN discussionSubmitted What is the point of formalising mathematics? as a story · 5 points
HN discussion
