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

21–30 of 230 posts

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

#21

Post by throwalean »

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…

Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-;

Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138

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

#22

Post by lmm »

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?

In theory yes. In practice mathematicians tend to have a good instinct for which things are true (although not always - some false theorems stood for decades if not centuries) and will avoid looking into ideas that don't pass the sniff test. Plus if you keep building on the consequences of a false result then you'll likely eventually reach a contradiction, which might inspire you to spot the bug in the original result.

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

#23

Post by pjmlp »

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…

Or using F* and then generate F# code, https://www.fstar-lang.org/

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

#24

Post by throwalean »

woolion wrote: post #19
Dudester230602 wrote: post #9

I was worried that Lean4 is a yet another LLM, but it's actually some hard and reliable stuff.

"Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.

"Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.

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

#25

Post by [deleted] »

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…

[deleted]

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

#26

Post by tux3 »

ohduran wrote: post #17
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.

I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically.

Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verified math that people can contribute to and use in new proofs.

A big multi-year effort to start formalizing the proof of Fermat's Last Theorem in Lean 4 was approved recently: https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_F...

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

#27

Post by eigenket »

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?

Yes! I work in quantum information theory and this recently happened in a subfield called resource theories.

The generalised quantum Stein's lemma [1][2] is (or was) a very powerful result that was used for over 10 years to prove things in this subfield. However last year it was noticed that there was an error in the proof of this lemma, and a whole bunch of results based on it weren't valid [3][4]. One of the authors of the paper where they wrote about the error gave a talk at the conference QIP 2023 this year, and there is a video of that talk available here [5]. Bartosz is a good speaker and I recommend watching the talk if you're interested, if you go to about 10 minutes, 30 seconds in the talk he discusses the consequences of this result now being not known to be true.

[1] Published paper https://link.springer.com/article/10.1007/s00220-010-1005-z

[2] Arvix version: https://arxiv.org/abs/0904.0281

[3] Published version: https://quantum-journal.org/papers/q-2023-09-07-1103/

[4] Arxiv version: https://arxiv.org/abs/2205.02813

[5] Youtube link: https://www.youtube.com/watch?app=desktop&v=2Xyodvh6DSY

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

#29

Post by throw_pm23 »

rey0927 wrote: post #8
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…

some claim his intelligence is the highest ever measured

He's a great mathematician all right, but that is a very silly way to put it.

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

#30

Post by eigenket »

isaacfrond wrote: post #18
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.

The theorem was mostly correct. As stated it was false, but it was true for n >= 8. If you change some not very interesting constants it becomes true for all n. All you need change is the constants for n < 8.
Post reply on HN