Lean4 helped Terence Tao discover a small bug in his recent paper
1–10 of 230 posts
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#2A few years back, I was trying to find out how to reduce mistakes in the programs I write.
I got introduced to Lamport's TLA+ for creating formal specifications, thinking of program behaviors in state machines. TLA+ taught me about abstraction in a clear manner.
Then I also discovered the book series "software foundations", which uses the Coq proof assistant to build formally correct software. The exercises in this book are little games and I found them quite enjoyable to work through.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#3For 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.
> 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 Carol Collins chair.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#4For 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…
Field's Medal winner.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#5Is it possible that small bugs or assumptions in a root paper could cascade through referencing papers leading to wildly inaccurate outcomes 5 or 6 papers down the line?
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#6For 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…
It's correct that he is a professor at UCLA, but it's also worth mentioning that he's regularly called nicknames like 'greatest mathematician alive' (just try googling that phrase): https://academicinfluence.com/rankings/people/most-influenti...
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#7Is it possible that small bugs or assumptions in a root paper could cascade through referencing papers leading to wildly inaccurate outcomes 5 or 6 papers down the line?
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#8For 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…
some claim his intelligence is the highest ever measured
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#9I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#10Lean4 is brilliant. Worth digging into as a programmer. Coq, Lean4, Agda etc. made my brain explode in a good way. Making me a better software developer.