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

11–20 of 230 posts

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

#11

Post by thfuran »

GEBBL wrote: post #5

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

I work in medical software and a few years ago fixed a bug that was an incorrect parameter value in a model used for computing diagnostic criteria that had proliferated throughout the literature after seemingly being incorrectly transcribed in one influential paper. The difference was relatively small, but it did make results somewhat worse.

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

#12

Post by gridentio »

deterministic wrote: post #10

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

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.

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

#13

Post by Genbox »

atomicnature wrote: post #2

A 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 b…

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.

C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.

The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].

[1] https://www.microsoft.com/en-us/research/project/code-contra...

[2] https://github.com/Z3Prover/z3

[3] https://github.com/microsoft/CodeContracts

[4] https://github.com/dafny-lang/dafny

[5] https://github.com/dotnet/csharplang/issues/105

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

#14

Post by chx »

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…

Tao got his PhD at the age of 21 and a tenured professor chair at the age of 24. To compare, at the age of 21 ordinary people only get their bachelors and typically it's 23-24 they when they get their masters degree. A PhD takes several more years and of course very few become tenured professors even more years later.

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

#16

Post by mjburgess »

Genbox wrote: post #13
atomicnature wrote: post #2

A 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 b…

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checke…

The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level.

Certain sorts of algorithmically complex development (games, cars, medical hardware, etc.) would benefit from a 'closed-world verification' -- but that's not most software, and they have alternatives.

'Code correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end.

The effort to source-level-check source-level-code is largely a huge waste of time and creates an illusion of reliability which rarely exists.

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

#17

Post by ohduran »

tux3 wrote: post #15

For people looking for an easy introduction to Lean4, the Natural Number Game is great: https://adam.math.hhu.de/#/g/hhu-adam/NNG4 And if you just want to read without playing a game: https://lean-lang.org/theorem_proving_in_lean4/introduction....

Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison?

Edit: Wrote Allow the first time, good stuff.

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

#18

Post by isaacfrond »

GEBBL wrote: post #5

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

More likely, wildly inaccurate outcomes will cause a re-examination of the cited theorems, which will probably flush out the bug.

By the way it is not clear to me, if the theorem was false or if only proof was wrong.

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

#20

Post by pjmlp »

chx wrote: post #14
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…

Tao got his PhD at the age of 21 and a tenured professor chair at the age of 24. To compare, at the age of 21 ordinary people only get their bachelors and typically it's 23-24 they when they get their masters degree. A PhD takes several more years and of course very few become tenured professors even more years later.

Depends on the country, before Bologna Portuguese degrees would be 5 years, so 23-24 would be the age of finalizing the degree, given that PhD without Msc wasn't possible back then, having everything done meant at least 30.
Post reply on HN