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

Lean4 helped Terence Tao discover a small bug in his recent paper

mathstodon.xyz

Post reply on HN
Print view View original

71–80 of 230 posts

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#71

Post by jvm___ »

j7ake wrote: post #39
SushiHippie wrote: post #3

For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Ca…

Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.

If you're going for a PhD or researching some obscure, furthest reach study of some mathematical principle and you get stuck. One of the ways to move forward is to hope that Terence Tao finds your topic interesting and can give you a few minutes of his time - because he'll probably have some ideas for moving your research forward.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#72

Post by btreecat »

j7ake wrote: post #39
SushiHippie wrote: post #3

For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Ca…

Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.

So that's an excuse for such a low context post?

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#73

Post by 0xpgm »

Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase?

Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#74

Post by [deleted] »

j7ake wrote: post #39
SushiHippie wrote: post #3

For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Ca…

Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.

[deleted]

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#76

Post by logicchains »

0xpgm wrote: post #73

Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.

>Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase

Running a JavaScript codebase through the Typescript compiler is a lightweight way to do incremental proof checking, albeit it can only check proofs about the soundness of the code.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#77

Post by staunton »

cubefox wrote: post #44

I wonder whether we could combine formal proof checkers (like the Lean proof checker) with language models that generate synthetic conjecture-proof pairs in a formal language like Lean. The Lean proof checker could be used to automatically verify whether the synthetic proofs written by the language model are correct. This information could be used to provide an RL reward signal applied to the original language model,…

There are people doing this already. For Lean, an example is https://morph.so/blog/the-personal-ai-proof-engineer/

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#78

Post by staunton »

ykonstant wrote: post #53
gridentio wrote: post #12

Earlier quoted context omitted.

I'm kind of interested in how useful Lean4 is as a programming language, and if it's easy to prove things about a program written in Lean. I should probably look into that when I have a minute.

Regarding usefulness: Lean is very nice to program in, if you care about pure functional languages; its FFI allows you to incorporate fast C routines very easily if pure Lean is not performant enough or lacks features. However, in some domains, Lean is within a decimal order of magnitude of (not hand-optimized) C; some benchmarks I hand-made recently impressed me. Regarding proving things about programs, no, it is no…

> the developers do not seem to consider it a core goal of Lean

I guess it depends on who you ask. The original devs of Lean wanted to do "everything" (because that's how you start projects, I guess). Since then it has attracted a lot of mathematicians (especially those working on Mathlib, a library that aspires to formalize "all known math") who are happy to have "algorithm objects" and prove things about them without being able to actually run an algorithm on any input.

This goes together with mostly embracing classical logic (which breaks the original and most powerful version of Curry-Howard, which allowed you to extract programs from proofs). However, in practical situations, algorithms extracted in this way tend to be too slow to be useful, so maybe that's not actually a downside for programming purposes.

Finally, Lean4 "compiles" to C-code, so at least it is (or can reasonably easily be made) portable. People have been trying to use it for real applications, like the AWS stuff others have linked in this thread.

Re: Lean4 helped Terence Tao discover a small bug in his recent paper

#80

Post by zozbot234 »

opan wrote: post #58
SushiHippie wrote: post #3

For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Ca…

I'm relieved that Lean4 doesn't seem to be some AI thing.

Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.
Post reply on HN