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

61–70 of 70 posts

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

#61

Post by jojomodding »

mycall wrote: post #28
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,…

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

Both type and set theory are formal logic, I don't see how that's what being argued. Rather that there are some things that are formal-logicy (e.g. set theory) and many other things that are not (like e.g. biology, you'll always find some weird organism breaking your assumptions).

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

#62

Post by anon291 »

cess11 wrote: post #41
anon291 wrote: post #35

Earlier quoted context omitted.

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

I'm not so sure, because Prolog.

Prolog is not a theorem prover. Theorem provers are total (I.e. not turing complete)

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

#63

Post by Gehinnn »

pvillano wrote: post #53
Gehinnn wrote: post #34

Earlier quoted context omitted.

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?

There have been bugs in Lean that allowed people to prove False, from which you can prove anything (they have been fixed).

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.

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

#64

Post by awesomeMilou »

oggy wrote: post #47
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…

In 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 s…

I'm curious since I'm not a mathematician: What do you mean by "stuck for a couple of weeks"? I am trying to practice more advanced math and have stumbled over lean and such but I can't imagine you just sit around for weeks to ponder over a problem, right? What do you do all this time?

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

#65

Post by nextos »

anon291 wrote: post #35
throwaway2027 wrote: post #3

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

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

There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.

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

#66

Post by namibj »

awesomeMilou wrote: post #64
oggy wrote: post #47

Earlier quoted context omitted.

In 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 s…

I'm curious since I'm not a mathematician: What do you mean by "stuck for a couple of weeks"? I am trying to practice more advanced math and have stumbled over lean and such but I can't imagine you just sit around for weeks to ponder over a problem, right? What do you do all this time?

Experience counter examples for why a specific definition is not going to work. Many times, at various levels of "not going to", usually hovering slightly above a syntactic level, but sometimes hovering on average above a plain definition semantic level, i.e. being mostly concerned with some indirect interaction aspects.

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

#67

Post by cess11 »

anon291 wrote: post #62
cess11 wrote: post #41

Earlier quoted context omitted.

I'm not so sure, because Prolog.

Prolog is not a theorem prover. Theorem provers are total (I.e. not turing complete)

"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

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.

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

#68

Post by deterministic »

nextos wrote: post #59
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.

Completely agree. Refinement types is a much more practical tool for software developers focusing on writing real world correct code.

Using LEAN or Coq requires you to basically convert your code to LEAN/Coq before you can start proving anything. And importing some complicated Hoare logic library. While proving things correct in Dafny (for example) feels much more like programming.

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

#69

Post by anon291 »

nextos wrote: post #65
anon291 wrote: post #35

Earlier quoted context omitted.

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

There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.

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

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

#70

Post by oggy »

awesomeMilou wrote: post #64
oggy wrote: post #47

Earlier quoted context omitted.

In 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 s…

I'm curious since I'm not a mathematician: What do you mean by "stuck for a couple of weeks"? I am trying to practice more advanced math and have stumbled over lean and such but I can't imagine you just sit around for weeks to ponder over a problem, right? What do you do all this time?

I'm not a mathematician either ;) Yeah, I won't sit around and ponder at a property definition for weeks. But I will maybe spend a day on it, not get anywhere, and then spend an hour or two a day thinking about ways to formulate it. Sometimes I try something, then an hour later figure out it won't work, but sometimes I really do just stare at the ceiling with no idea how to proceed. Helps if you have someone to talk to about it!
Post reply on HN