Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lean 4: How the theorem prover works and why it's the new competitive edge in AI

venturebeat.com

Post reply on HN
Print view View original

51–60 of 70 posts

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#51

Post by whattheheckheck »

YeGoblynQueenne wrote: post #40
Rochus wrote: post #22

Interesting. It's essentially the same idea as in this article: 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,…

>> 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). 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 informati…

Reasoning is a pattern that is embedded within the token patterns but the llms are imitating reasoning via learning symbolic reasoning patterns.

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

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#52

Post by [deleted] »

lo_zamoyski wrote: post #37
seanhunter wrote: post #13

Earlier quoted context omitted.

Yes 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 a…

Technically, 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]

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#53

Post by pvillano »

Gehinnn wrote: post #34
nwyin wrote: post #31

Earlier quoted context omitted.

it'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

This 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).

Do 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?

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#54

Post by daxfohl »

upghost wrote: post #39

So 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 ne…

Yeah, even for simple things, it's surprisingly hard to write a correct spec. Or more to the point, it's surprisingly easy to write an incorrect spec and think it's correct, even under scrutiny, and so it turns out that you've proved the wrong thing.

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).

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#55

Post by sinkasapa »

Rochus wrote: post #22

Interesting. It's essentially the same idea as in this article: 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,…

Lean 4 is uses constructive logic. If a closed world assumption requires that a statement that is true is also known to be true, and that any statement that is not known to be true is therefore false, that is not true of constructive systems. I only use Rocq, but I believe the type theories in Rocq and Lean 4 are basically similar variations on the Calculus of Constructions in both cases, though there are important differences. In a constructive theory something is true if a proof can be constructed, but the lack of a proof does not entail that something is false. One needs to prove that something is false. In constructive type theory, one can say, that something is true or false.

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#56

Post by emih »

Machine 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.

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#57

Post by bwestergard »

emih wrote: post #56

Machine 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…

Yes.

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.

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#58

Post by fauigerzigerk »

daxfohl wrote: post #54
upghost wrote: post #39

So 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 ne…

Yeah, even for simple things, it's surprisingly hard to write a correct spec. Or more to the point, it's surprisingly easy to write an incorrect spec and think it's correct, even under scrutiny, and so it turns out that you've proved the wrong thing. 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'…

>But I'm not super bullish on "proofs" being the thing that keeps AI in line.

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.

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#59

Post by nextos »

upghost wrote: post #39

So 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 ne…

As a heavy user of formal methods, I think refinement types, instead of theorem proving with Lean or Isabelle, is both easier and more amenable to automation that doesn't get into these pitfalls.

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.

Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI

#60

Post by daxfohl »

fauigerzigerk wrote: post #58
daxfohl wrote: post #54

Earlier quoted context omitted.

Yeah, even for simple things, it's surprisingly hard to write a correct spec. Or more to the point, it's surprisingly easy to write an incorrect spec and think it's correct, even under scrutiny, and so it turns out that you've proved the wrong thing. 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'…

>But I'm not super bullish on "proofs" being the thing that keeps AI in line. 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.

Code review, tests, a planning step to make sure it's approaching things the right way, enough experience to understand the right size problems to give it, metrics that can detect potential problems, etc. Same as with a junior engineer.

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.

Post reply on HN