Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • Examples 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

    by westurner
  • I guess I'm missing something but I don't see how this isn't just:

    1. Creating more work 2. Shifting the existing work to specification

    There's not really such a thing as a perfect specification. One of the things AI is taking away is character by character feedback cycles. Can't count how many times I'll be writing software and think in the middle of writing a return, realize this is probably not what I should be doing. I'm not sure how you would really replicate that experience when creating specs... nobody is going to sit and meditate on their specs for hours before writing them.

    by robswc
  • I just don’t know why we are using a verification that is hard to read and write for humans
    by charlieyu1
  • Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean would ensure that the translation is correct.
    by fspeech
  • If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?
    by beecasthurlbow
  • > ... But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.

    Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)

    by PandaRider
  • What do people think of property based testing? I’ve set up a few property based tests and it feels almost like formal verification.

    I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious setup, but LLMs solve that.

    I haven’t seen much discussion around PBTs lately, but you get a ton of bang for your buck in the LLM age

    by chamomeal
  • I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.

    This is how formal methods can constrain AI for large systems.

    We're doing this at the Open Markets Initiative, where we've generated millions of lines of Lean 4, TLA+, and Rocq that ensure that our open source electronic trading protocol code is accurate. We didn't expect it but the Lean prover did identify some incorrect steps. https://github.com/Open-Markets-Initiative

    by wbeckler

Explore Birbla archives