Top all-time · #19011
Tristan Stérin
Personal blog · tristan.st/blogaimath
Tristan Stérin's personal blog at tristan.st covers ai and math. Since 2026, 4 different Hacker News readers have linked it 5 times, most often “In search of falsehood – using Opus 4.6 to prove False”. It is still writing: the last post was on 2026-03-05, and you can follow it by feed.
Too few sampled comments (1) to say how often HN recommends it.?
Why HN links it
HN readers cite this blog as a source for bug counts in proof systems, in a thread on how small trusted proof kernels are. The posts concern formal proof systems and bugs found in them.
Summarised by Claude from a sample of 1 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Most-linked posts?
- In search of falsehood – using Opus 4.6 to prove False2 people · 2 mentions · first linked 2026-03-18
What Hacker News says?
Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m... Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood
Comment linking /blog/in_search_of_falsehood
on “Are We Stuck with Lean?”Submitted In search of falsehood – using Opus 4.6 to prove False as a story · 2 points
HN discussionSubmitted Collatz Wang Tiles as a story · 1 points
HN discussionSubmitted Personal relationship with the bouba-kiki effect as a story · 1 points
HN discussionSubmitted Opus 4.6 is great at formal proofs (Rocq/Lean4) as a story · 1 points
HN discussion