Lean 4: How the theorem prover works and why it's the new competitive edge in AI
1–10 of 70 posts
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#2[flagged]
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#3I 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?
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#4[flagged]
Are you an AI just summarizing the article?
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#5I 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.
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#6[flagged]
Are you an AI just summarizing the article?
If 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.
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#7I 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?
It 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
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...
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#8I 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.
Lean has standard c ABI FFI support. https://lean-lang.org/doc/reference/latest/Run-Time-Code/For...
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#9I 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?
You 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.
Re: Lean 4: How the theorem prover works and why it's the new competitive edge in AI
#10Earlier quoted context omitted.
Are you an AI just summarizing the article?
If 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.
It is very rude as it just wastes everyone’s time and debases the commons. I’m pretty sure it’s also against the guidelines.