But Lean 4 is significantly more rigid, granular, and foundational than e.g. Event-B, and they handle concepts like undefined areas and contradictions very differently. While both are "formal methods," they were built by different communities for different purposes: Lean is a pure mathematician's tool, while Event-B is a systems engineer's tool. Event-B is much more flexible, allowing an engineer (or the LLM) to sketch the vague, undefined contours of a system and gradually tighten the logical constraints through refinement.
LLMs are inherently statistical interpolators. They operate beautifully in an Open World (where missing information is just "unknown" and can be guessed or left vague) and they use Non-Monotonic Reasoning (where new information can invalidate previous conclusions). Lean 4 operates strictly on the Closed World Assumption (CWA) and is brutally Monotonic. This is why using Lean to model things humans care about (business logic, user interfaces, physical environments, dynamic regulations) quickly hits a dead end. The physical world is full of exceptions, missing data, and contradictions. Lean 4 is essentially a return to the rigid, brittle approach of the 1980s expert systems. Event-B (or similar methods) provides the logical guardrails, but critically, it tolerates under-specification. It doesn't force the LLM to solve the Frame Problem or explicitly define the whole universe. It just checks the specific boundaries the human cares about.
I think LLM reasoning is not so much non-monotonic as unsound, in the sense that conclusions do not necessarily follow from the premises. New information may change conclusions but how that happens is anyone's guess. There's some scholarship on that, e.g. there's a series of papers by Subarao Kamphampathi and his students that show how reasoning models' "thiking" tokens don't really correspond to sound reasoning chains, even if they seem to improve performance overall [1].
But it is difficult to tell what reasoning really means in LLMs. I believe the charitable interpretation of claims about LLM reasoning is that it is supposed to be informal. There is evidence both for and against it (e.g. much testing is in fact on formal reasoning problems, like math exam questions or Sokoban, but there's tests of informal reasoning also, e.g. on the bar exam). However, different interpretations are hard to square with the claims that "we don't understand reasoning"; not a direct quote, but I'm aware of many claims like that by people whose job it is to develop LLMs and that were made at the height of activity around reasoning models (which seems now to have been superseded by activity around "world models") [1].
If LLMs are really capable of informal reasoning (I'm not necessarily opposed to that idea) then we really don't understand what that reasoning is, but it seems we're a bit stuck because to really understand it, we have to, well, formalise it.
That said, non-monotonic reasoning is supposed to be closer to the way humans do informal reasoning in the real world, compared to classical logic, even though classical logic started entirely as an effort to formalise human reasoning; I mean, with Aristotle's Syllogisms (literally "rsasonings" in Greek).
________________
[1] Happy to get links if needed.
The very fact that it memorized the Ceasar cipher rot13 pattern is due to it being a Linux command and it had examples of patterns of 13 shifted letters. If you asked it to figure out a different shift it struggled.
Now compound that across all intelligent reasoning problems in the entirety of human existence and you'll see how we will never have enough data to make agi with this architecture and training paradigm.
But we will have higher and higher fidelity maps of symbolic reasoning patterns as they suck up all the agent usage data for knowledge work tasks. Hopefully your tasks fall out of distribution of the median training data scope
Over the past year, I went from fully manual mode (occasionally asking chat gpt some Lean questions) to fully automatic mode, where I barely do Lean proofs myself now (and just point AI to the original .tex files, in German). It is hard to believe how much the models and agentic harnesses improved over the last year.
I cannot describe how much fun it is to do refactorings with AI on a verified Lean project!
Also, it's so easy now to have visualizations and typesetted documents generated by AI, from dependency visualizations of proofs using the Lean reflection API, to visual execution traces of cellular automatas.
And here are some examples of the different philosophies of AI proofs and human proofs: https://gist.github.com/hediet/e3569a7c6b4b7c4f7d4a7db410104...
I use VS Code in a beefy Codespace, with GitHub Copilot (Opus 4.5). I have a single instruction file telling the AI to always run "lake build ./lean-file.lean" to get feedback.
(disclaimer: I work on VS Code)
Or is it as long as you formalize your theorem correctly, a valid lean program is an academically useful proof?
Are there any minimal examples of programs which claim to prove the thing without actually proving the thing in a meaningful way?
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution. The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.
Where it cannot (fully) replace humans, is writing the _theorems_ themselves. A human has to check that the theorem being proven is actually what you were trying to prove, and this is not safe from LLM hallucinations. If you ask an LLM, is this bridge safe, and it writes `Theorem bridge_is_safe : 1 + 1 = 2.` and proves this theorem, that does _not_ mean the bridge is safe...
The article then also makes some wild extrapolations:
> We could imagine an LLM assistant for finance that provides an answer only if it can generate a formal proof that it adheres to accounting rules or legal constraints.
I guess it's true because you could imagine this, hypothetically. But it's not going to happen, because you cannot formalize a financial or legal statement in a proof assistant. It's a fundamentally informal, real-world thing, and proof assistants are fundamentally for proving formal, abstract things.
Here is another way to think of this. We all understand that the value of a lawyer in contract negotiations lies not only in drafting a document that, when fed to judge, produces the desired outcome. Rather, lawyers help clients (and counterparties) decide on what their interests consist in.
Developing software is always something of a principal-agent coordination problem, and comes with transaction costs.
Much of the time, most of us labor under the illusion that each of us understands our desires and interests better than any other party could.
HOWEVER … I hit something i now call a McLuhen vortex error: “When a tool, language, or abstraction smuggles in an implied purpose at odds with your intended goal.”
Using Lean implies to the coding agent ‘proven’ is a pervasive goal.
I want to use lean to be more articulate about the goal. Instead using lean smuggled in a difficult to remove implicit requirement that everything everywhere must be proven.
This was obvious because the definitions i made in lean imply the exact opposite of everything needs to be proven. When i use morphism i mean anything that is a morphism not only things proven to be morphisms.
A coding agent driven by an llm needs a huge amount of structure to use what the math says rather than take on the implications that because it is using a proof system therefore everything everywhere is better if proven.
The initial way i used lean poisoned the satisficing structure that unfolds during a coding pass.
So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.
https://github.com/teorth/analysis
He also has blogged about how he uses lean for his research.
Edit to add: Looking at that repo, one thing I like (but others may find infuriating idk) is that where in the text he leaves certain proofs as exercises for the reader, in the repo he turns those into “sorry”s, so you can fork the repo and have a go at proving those things in lean yourself.
If you have some proposition which you need to use as the basis of further work but you haven’t completed a formal proof of yet, in lean, you can just state the proposition with the proof being “sorry”. Lean will then proceed as though that proposition had been proved except that it will give you a warning saying that you have a sorry. For something to be proved in lean you have to have it done without any “sorry”s. https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tac...
Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.
- Lean supports calling out as a tactic, allowing you to call LLMs or other AI as judges (ie, they return a judgment about a claim)
- Lean can combine these judgments from external systems according to formal theories (ie, normal proof mechanics)
- an LLM engaged in higher order reasoning can decompose its thinking into such logical steps of fuzzy blocks
- this can be done recursively, eg, having a step that replaces LLM judgments with further logical formulations of fuzzy judgments from the LLM
Something, something, sheaves.
This misses a point that software engineers initmately know especially ones using ai tools:
* Proofs are one QA tool
* Unit tests, integration tests and browser automation are other tools.
* Your code can have bugs because it fails a test above BUT...
* You may have got the requirements wrong!
Working with claude code you can have productive loops getting it to assist you in writing tests, finding bugs you hadn't spotted and generally hardening your code.
It takes taste and dev experience definitely helps (as of Jan 26)
So I think hallucinations and proofs as the fix is a bit barking up the wrong tree
The solution to hallucinations is careful shaping of the agent environment around the project to ensure quality.
Proofs may be part of the qa toolkit for AI coded projects but probably rarely.
This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.
So no way of leveraging an existing ecosystem.
“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“
My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.
I find it very surprising that nobody tried to make something like gRPC as an interop story for a new language, with an easy way to write impure "extensions" in other languages and let your pure/formal/dependently typed language implement the rest purely through immutable message passing over gRPC boundary. Want file i/o? Implement gRPC endpoint in Go, and let your language send read/write messages to it without having to deal with antiquated and memory unsafe Posix layer.
[1] https://old.reddit.com/r/totallynotrobots
PS: Of course that's not true. An ID system for humans will inevitably become mandatory and, naturally, politicians will soon enough create a reason to use it for enforcing a planet wide totalitarian government watched over by Big Brother.
Conspiracy-theory-nonsense? Maybe! I'll invite some billionaires to pizza and ask them what they think.
What's the HN stance on AI bots? To me it just seems rude - this is a space for people to discuss topics that interest them & AI contributions just add noise.
I realize formal verification with lean is a slightly different game but if anyone here has any insight, I tend to be extremely nervous about a confidently presented AI "proof" because I am sure that the proof is proving whatever it is proving, but it's still very hard for me to be confident that it is proving what I need it to prove.
Before the dog piling starts, I'm talking specifically about distributed systems scenarios where it is just not possible for a human to think through all the combinatorics of the liveness and safety properties without proof assistance.
I'm open to being wrong on this, but I think the skill of writing a proof and understanding the proof is different than being sure it actually proves for all the guarantees you have in mind.
I feel like closing this gap is make it or break it for using AI augmented proof assistance.
But it's still usually possible to distill a few crucial properties that can be specified in an "obviously correct" manner. It takes A LOT of work (sometimes I'd be stuck for a couple of weeks trying to formalize a property). But in my experience the trade off can be worth it. One obvious benefit is that bugs can be pricey, depending on the system. But another benefit is that, even without formal verification, having a few clear properties can make it much easier to write a correct system, but crucially also make it easier to maintain the system as time goes by.
There was a post a few months ago demonstrating this for various "proved" implementations of leftpad: https://news.ycombinator.com/item?id=45492274
This isn't to say it's useless; sometimes it helps you think about the problem more concretely and document it using known standards. But I'm not super bullish on "proofs" being the thing that keeps AI in line. First, like I said, they're easy to specify incorrectly, and second, they become incredibly hard to prove beyond a certain level of complexity. But I'll be interested to watch the space evolve.
(Note I'm bullish on AI+Lean for math. It's just the "provably safe AI" or "provably correct PRs" that I'm more skeptical of).
But do we have anything that works better than some form of formal specification?
We have to tell the AI what to do and we have to check whether it has done that. The only way to achieve that is for a person who knows the full context of the business problem and feels a social/legal/moral obligation not to cheat to write a formal spec.
If you want something fully automated, then I think more investment in automating and improving these capabilities is the way to go. If you want something fully automated and 100% provably bug free, I just don't think that's ever going to be a reality.
Formal specs are cryptic beyond even a small level of complexity, so it's hard to tell if you're even proving the right thing. And proving that an implementation meets those specs blows up even faster, to the point that a lot of stuff ends up being formally unprovable. It's also extremely fragile: one line code change or a small refactor or optimization can completely invalidate hundreds of proofs. AI doesn't change any of that.
So that's why I'm not really bullish on that approach. Maybe there will be some very specific cases where it becomes useful, but for general business logic, I don't see it having useful impact.
It's less powerful, but easier to break down and align with code. Dafny and F* are two good showcases. Less power makes it also faster to verify and iterate on.
In the case of digital systems it can be much worse because we often have to include many assumptions to accommodate the complexity of our models. To use an example from your context, usually one is required to assume some kind of fairness to get anything to go through with systems operating concurrently but many kinds of fairness are not realistic (eg strong fairness).