alt Hacker NewsExamples of comparing the results of Lean and e.g. Rust as is described in the video?
I have symbolic error terms in Lean that I guess can be sampled and compared to Monte Carlo analysis? But I already had sampling-based analysis, that's why I had to do all of this (double-slit experiment and gravity with GrC(2,4)) in Lean 4.
What would it take to combine Lean and one or more Rust TLA+ implementations? How does an agent plan and implement this and what are the advantages and disadvantages?
"Comparison of Isabelle/HOL, Lean, HOL4, and Agda: A Tale of Four Theorem Provers" (2026) but not Rocq? https://news.ycombinator.com/item?id=50043202
Nice article, here is the direct link since no one commented on the HN post.
A tale of four theorem provers - https://blueberrywren.dev/blog/primes/
> Broadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. forall x, x = x) that all proofs must be constructed via.
In all my years of reading - and I've written my fair share of dangling prepositions - this is the first time seeing "via" at the end of a sentence. Let me guess the author is German, Danish, or a mathematician.
These abbreviations were not defined before use.
- LCF: Logic for Computable Functions - https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
- HOL: Higher Order Logic - https://en.wikipedia.org/wiki/HOL_(proof_assistant)