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

31–40 of 230 posts

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

#31

Post by pbhjpbhj »

lmm wrote: post #22
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 resul…

If mathematicians have "a good instinct" does that suggest that their brains can somehow apply an informal proof?

I wonder if they are good, or if it's selection/confirmation/other biases that lead is to think say.

Also, aren't surprising results the most interesting!?

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

#32

Post by aeonik »

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…

Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming.

Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.

https://github.com/idris-lang/Idris2

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

#33

Post by ohduran »

tux3 wrote: post #26
ohduran wrote: post #17

Earlier quoted context omitted.

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 verifi…

Thank you so much for your answer

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

#35

Post by mrkeen »

mjburgess wrote: post #16
Genbox wrote: post #13

Earlier quoted context omitted.

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…

Strong disagree.

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

The choice to run a system as many different moving parts is a decision taken by the team in order to avoid failure.

> Certain sorts of algorithmically complex development -- but that's not most software

It's all software.

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

No and no. I have comprehensive end-to-end tests. They take forever, don't fit into RAM (for some services I need to run them on my home PC because my work laptop only has 16GB), and most importantly: they show that the code is not correct. Now I have to change incorrect code to correct code (while not breaking any public interfaces. I wish my predecessors did not put incorrect code into the live system.

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

#36

Post by forward-slashed »

Also check out Morph Labs, which is working with Lean to create an AI proof assistant. Cool startup by ex-OpenAI folks.

Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment.

https://x.com/morph_labs

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

#37

Post by eigenket »

pbhjpbhj wrote: post #31
lmm wrote: post #22

Earlier quoted context omitted.

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 resul…

If mathematicians have "a good instinct" does that suggest that their brains can somehow apply an informal proof? I wonder if they are good, or if it's selection/confirmation/other biases that lead is to think say. Also, aren't surprising results the most interesting!?

In an informal sense disproving things is easier than proving things. For example theorems often say thing like "all objects of type Y have property X", its very difficult to work out even where to start proving such a statement unless you're an expert in Y and X, but to disprove it all you have to do is find some example Y which doesn't have property X. If you've worked with Y things for a while you probably have a bunch of "pet" Y objects you can think of and if someone proves something you kinda automatically check to see what their proof says about the ones you're familiar with.

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

#38

Post by pas »

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…

Kevin Buzzard (a professional mathematician) has a few good talks about Lean

https://youtu.be/Dp-mQ3HxgDE from 2019 at MS Research

https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s (2022 at ICM international math congress)

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

#39

Post by j7ake »

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.

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

#40

Post by n4r9 »

pjmlp wrote: post #20
chx wrote: post #14

Earlier quoted context omitted.

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.

In the other direction, in the UK it's quite possible to have your bachelors by 21, masters by 22 and PhD by 25. I had my mathematics PhD by 26 and am not a remarkable mathematician.
Post reply on HN