5 ms·
Lean 4: How the theorem prover works and why it's the new competitive edge in AI
- tesserato 8mo ago[flagged]
- nudpiedo 8mo agoAre you an AI just summarizing the article?
- pja 8mo agoIf you look at their comment history it's quite clear that's what they are. 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.
- seanhunter 8mo agoIt is very rude as it just wastes everyone’s time and debases the commons. I’m pretty sure it’s also against the guidelines.
- throwaway2027 8mo agoI think I saw Terence Tao use a formal proof language but I don't remember if it was Lean. I'm not familiar with it but I do agree that moving to provable languages could improve AI but isn't the basis just having some immutable rigorous set of tests basically which could be replicated in "regular" programming languages?
- seanhunter 8mo agoIt was lean4. In fact he has made lean4 versions of all of the proofs in his Analysis I textbook available here https://github.com/teorth/analysis 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/Tactic-Reference/#sorry https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tac...
- iNic 8mo agoYou can think of theorem provers as really crazy type checkers. It's not just a handful of tests that have to run, but more like a program that has to compile.
- seanhunter 8mo agoYes exactly. There is this thing called the “Curry-Howard Isomorphism” which (as I understand it) says that propositions in formal logic are isomorphic to types. So the “calculus of constructions” is a typed lambda calculus based on this that makes it possible for you to state some proposition as a type and if you can instantiate that type then what you have done is isomorphic to proving the proposition. Most proof assistants (and certainly Lean) are based on this. 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.
- lo_zamoyski 7mo agoTechnically, it isn't an isomorphism (the word is abused very often), and there is no fixed, general syntactic correspondence. However, in the case of Lean, we can establish a correspondence between its dependent type system and intuitionistic higher-order predicate logic.
- deleted 7mo ago[deleted]
- gaogao 8mo agoYes, though often the easiest way to replicate it in regular programming languages is to translate that language to Lean or another ITM, though auto-active like Verus is used for Rust pretty successfully. 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.
- anon291 7mo agoA theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no testing involved.
- cess11 7mo agoI'm not so sure, because Prolog.
- anon291 7mo agoProlog is not a theorem prover. Theorem provers are total (I.e. not turing complete)
- cess11 7mo ago"Is Prolog a theorem prover? Richard O'Keefe said it best: Prolog is an efficient programming language because it is a very stupid theorem prover." https://www.metalevel.at/prolog/theoremproving https://www.metalevel.at/prolog/theoremproving Who am I to overrule the author of The Craft of Prolog? Some would say that SLDNF resolution qualifies as theorem proving, some would disagree and say that a theorem prover also needs such and such capability. Anyway, as Triska shows above you can implement software that is quite a lot like a theorem prover in about thirty lines of Prolog, i.e. not "a dependently typed functional programming language". The descendants of Milner's work, notably ML and the Edinburgh LCF theorem prover, have been quite successful, though.
- nextos 7mo agoThere are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.
- anon291 7mo agoWeakly typed, but strongly kinded. It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed. Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.
- nudpiedo 8mo agoI like a lot of the idea behind such theorem provers, however, I always have issues with them producing compatible code with other languages. 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.
- seanhunter 8mo agoLean has standard c ABI FFI support. https://lean-lang.org/doc/reference/latest/Run-Time-Code/Foreign-Function-Interface/ https://lean-lang.org/doc/reference/latest/Run-Time-Code/For...
- nudpiedo 8mo agoLiterally the first line of the link: “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.
- densh 7mo agoApart from prioritizing FFI (like Java/Scala, Erlang/Elixir), the other two easy ways to bootstrap an integration of a new obscure or relatively new programming language is to focus on RPC (ffi through network) or file input-output (parse and produce well known file formats to integrate with other tools at Bash level). 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.
- AxiomLab 8mo ago[flagged]
- zmgsabst 8mo agoThe real value is in mixed mode: - 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.
- xvilka 8mo agoLean is a great idea, especially the 4th version, a huge level up from the 3rd one, but its core still deficient[1] in some particular scenarious (see an interesting discussion[2] in the Rock (formerly Coq) issue tracker). Not sure if it might hinder the automation with the AI. [1] https://artagnon.com/logic/leancoq https://artagnon.com/logic/leancoq [2] https://github.com/rocq-prover/rocq/issues/10871 https://github.com/rocq-prover/rocq/issues/10871
- joomy 7mo agoThe issue was a fun read, thanks for sharing.
- Gehinnn 7mo agoI just completed the formal verification of my bachelor thesis about real time cellular automata with Lean 4, with heavy use of AI. 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.
- svara 7mo agoCan you give some examples of this? Maybe have something online? I would love to learn more about how to do proof driven AI assisted development.
- nwyin 7mo agoit's a bit dated, but Terence Tao has a video of formalizing a proof with LLMs from 9 months ago which should be illuminating https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq https://youtu.be/zZr54G7ec7A?si=-l3jIZZzfghoqJtq
- Gehinnn 7mo agoThis is very similar to how I worked with Lean a year ago (of course in a much simpler domain) - mostly manual editing, sometimes accepting an inline completion or next edit suggestion. However, with agentic AI that can run lean via CLI my workflow changed completely and I rarely write full proofs anymore (only intermediate lemma statements or very high level calc statements).
- pvillano 7mo agoDo lean poofs need to be manually reviewed? 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?
- kig 7mo agoIf you want to mess with this at home, I've been vibe coding https://github.com/kig/formalanswer https://github.com/kig/formalanswer to plug theorem provers into an LLM call loop. It's pretty early dev but it does have a logic rap battle mode.
- nl 7mo agoThis is pretty interesting!
- tokenless 7mo ago> Large language models (LLMs) have astounded the world with their capabilities, yet they remain plagued by unpredictability and hallucinations – confidently outputting incorrect information. In high-stakes domains like finance, medicine or autonomous systems, such unreliability is unacceptable. 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.
- Rochus 7mo agoInteresting. It's essentially the same idea as in this article: https://substack.com/home/post/p-184486153 https://substack.com/home/post/p-184486153. In both scenarios, the human is relieved of the burden of writing complex formal syntax (whether Event-B or Lean 4). The human specifies intent and constraints in natural language, while the LLM handles the work of formalization and satisfying the proof engine. 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.
- mycall 7mo agoSo basically you are arguing a Type Theory vs Set Theory problem, Foundationalism or Engineering Refinement. Since we read here of multiple use cases for LLMs in both CS divides, we can conclude an eventual convergence in these given approaches; and if not that, some formal principles should emerge of when to use what.
- Rochus 7mo agoThis discussion started already in the sixties (see e.g. the 1969 publication by McCarthy and Hayes where they describe the "frame problem" as a fundamental obstacle to the attempt to model the dynamic world using First-Order Logic and monotonic reasoning). A popular attempt to "solve" this problem is the Cyc project. Monotonic logic is universally understood as a special, restricted case (a subset) of a broader non-monotonic theory.
- SteveJS 7mo agoI am using lean as part of the prd.md description handed to a coding agent. The definitions in lean compile and mean exactly what I want them to say. The implementation i want to build is in rust. 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.
- lo_zamoyski 7mo agoThis has been the approach taken by some using LLMs, even in less type-heavy situations. Of course, it is part of a broader tradition in which search is combined with verification. Genetic programming and related areas come to mind. Here, LLMs are search, while Lean is used to express constraints.
- upghost 7mo agoSo I have been doing formal specification with TLA+ using AI assistance and it has been very helpful AFTER I REALIZED that quite often it was proving things that were either trivial or irrelevant to the problem at hand (and not the problem itself), but difficult to detect at a high level. 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.
- esafak 7mo agoCould you write a blog post about your experience to make it more concrete?
- johnbender 7mo agoYou have identified the crux of the problem, just like mathematics writing down the “right” theorem is often half or more of the difficulty. 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).
- oggy 7mo agoIn my experience, finding the "correct" specification for a problem is usually very difficult for realistic systems. Generally it's unlikely that you'll be able to specify ALL the relevant properties formally. I think there's probably some facet of Kolmogorov complexity there; some properties probably cannot be significantly "compressed" in a way where the specification is significantly shorter and clearer than the solution. 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.
- whattheheckheck 7mo agoWhy is lean4 so slow with the main math package
- 45dsilicon 7mo ago[dead]
- emih 7mo agoMachine learning is definitely enabling writing _proofs_ within a proof assistant, and I'm sure it will help to make formal verification more viable in the future. 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.
- bwestergard 7mo agoYes. 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.