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

121–130 of 230 posts

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

#121

Post by valyagolev »

skulk wrote: post #115
valyagolev wrote: post #109

Earlier quoted context omitted.

I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have every…

Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.

Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point?

What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing

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

#122

Post by charcircuit »

snovv_crash wrote: post #120
mrkeen wrote: post #35

Earlier quoted context omitted.

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

Tests only show that it is correct for the sets of values and code paths you exercise. It's quite possible for other aspects to be incorrect, and this is what theorem provers like Coq help with.

If you have an incomplete or buggy specification Coq won't actually prove the absence of bugs.

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

#123

Post by bjornasm »

howenterprisey wrote: post #93
mettamage wrote: post #65

Earlier quoted context omitted.

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that o…

I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fai…

That is really interesting. Whish there was some better name for that, as I feel like it isn't that descriptive. However their benefit seem really obvious, saying that something is an areay, or even an array of integers is barely half the picture if in reality it is a array of length 5 of even integers to loan from your example. I guess you would try to implement it in other languages creating objects?

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

#124

Post by waythenewsgoes »

malwrar wrote: post #114
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.

Dumb question: how do people skip years like this in college. Like suppose you do know the material well already, does that just get recognized by the faculty at some point (you are noticed pre-college and get a faculty member interested in you? In college?) or would he have needed to specifically apply for that in some way? I ask in jealousy, I felt like my college put as many administrative barriers as possible to…

He had a lot of acclaim as a young mathematician, according to Wikipedia he was taking college level math at 9 years of age. At this level of talent I believe you begin to be courted by top universities similar to D1 athlete's, not only that, but you are likely genius-level smart, so sticking you in a classroom of people your age would be doing you an intellectual disservice, similar to sticking a college freshman in a 2nd grade classroom. At this level, you are probably seen as the next Newton or Gauss, and professors will want to attach themselves to you and work alongside you. At this point you bring a ton of value to the school just for attending and they won't mind if you are testing out of course material since they are just happy for you to be there for any length of time, and it just becomes more of a formality anyway.

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

#125

Post by kmill »

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…

Leo de Moura wants Lean 4 to be used for software verification too.

A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).

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

#126

Post by cubefox »

ykonstant wrote: post #51
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,…

This workflow is an explicit goal of the Lean 4 devs. The official Zulip chat has a channel dedicated to the interface between the two: https://leanprover.zulipchat.com/#streams/219941/Machine%20L...

That would be interesting, though this link requires an account.

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

#127

Post by kmill »

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 core Lean 4 developers do want proving properties about programs to be easy. In the short term maybe priorities have been elsewhere due to limited resources, but that doesn't mean they do not consider this to be a core goal. My understanding is that there are still some research-level problems here that need to be worked out. (Proving things about do notation is currently a real pain for example.)

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

#128

Post by cubefox »

staunton wrote: post #77
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/

If I understand this correctly, they want to use an AI model for "autoformalization", which sounds like "using a language model to translate natural language proofs into Lean proofs". Which is cool but much less ambitious than the self-train system I described above. I guess AI technology isn't yet far enough to make such a proposal work.

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

#129

Post by skulk »

valyagolev wrote: post #121
skulk wrote: post #115

Earlier quoted context omitted.

Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.

Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was…

> What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code

This doesn't even exist in TypeScript. If I change

    function foo(a: any) { return baz(a); }
to

    function foo(a: number) { return baz(a); }
whoever calls foo has to still prove (or assert) that the argument is a number.

Is that what you're after, asserting a dependent type? For example being able to change:

    function divByTwo(a: number): number { return a/2; }
to

    function divByTwo(a: even_number): number { return a/2; }
You want every place divByTwo is called to also automatically supply a proof that the argument is even?

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

#130

Post by Scaless »

malwrar wrote: post #114
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.

Dumb question: how do people skip years like this in college. Like suppose you do know the material well already, does that just get recognized by the faculty at some point (you are noticed pre-college and get a faculty member interested in you? In college?) or would he have needed to specifically apply for that in some way? I ask in jealousy, I felt like my college put as many administrative barriers as possible to…

For non-geniuses like myself, you can just ask to test out of some of the lower tier introduction courses. I got a typically 4-year degree in 3 years this way. It's called credit-by-examination.

I'm sure for the prodigy-level students there is an even higher streamlined process for keeping them engaged.

Post reply on HN