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

161–170 of 230 posts

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

#161

Post by gosub100 »

mettamage wrote: post #108
howenterprisey wrote: post #93

Earlier quoted context omitted.

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…

Because I had the question and I figured this was quicker. I didn’t know what dependent types were. So now you know why I do it. Also, I believe this is my first time doing it. I might be wrong. Is it better to ask and wait for an answer instead? There is nothing in the guidelines on HN about it. I don’t know what’s reasonable and I haven’t seen strong cultural norms from HN yet. I at least labeled that the text was…

> Is it better to ask and wait for an answer instead?

No, around here it's better to say "So dependent types are pretty much $SOMETHING_COMPLETLY_WRONG ?" and wait for all the "corrections" (aka Cunningham's law someone linked to nearby).

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

#162

Post by gosub100 »

xeonmc wrote: post #97
howenterprisey wrote: post #93

Earlier quoted context omitted.

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…

ChatGPT = Cunningham bait

I don't see anything wrong with GPT's answer other than pedantic quibbling. I just don't like it because I don't want to share this space with non-humans.

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

#163

Post by charcircuit »

Jweb_Guru wrote: post #157
charcircuit wrote: post #122

Earlier quoted context omitted.

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

This is true but mostly meaningless in practice. I have never found the people who say this every time formal verification comes up to be the same people who actually work in formal verification. The reality is that it's far far harder to mess up a formal spec that you actually have to prove a concrete instance of, than it is to mess up the code. With a buggy spec, in the course of trying to prove it you'll arrive at…

>Formal spec bugs happen, but they're quite rare

A lot of specs bugs happen all the time. If you think people can account for all edge cases in massively complex projects you are wrong. There are many behaviors that you can't predict will be nonsensical ahead of time until you actually hit them.

Formal verification is not a silver bullet. Despite all of the extra effort bugs will still happen. It's better to invest in making things safe by default, or by aborting when getting into a bad state.

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

#164

Post by gosub100 »

Jtsummers wrote: post #113
mettamage wrote: post #110

Earlier quoted context omitted.

What does that mean?

https://meta.wikimedia.org/wiki/Cunningham%27s_Law Cunningham's Law: Post something wrong online so you can get a correct answer. Half the ChatGPT answers on here seem to be wrong in obvious ways or, worse, subtle but critical ways. When people post them they get downvoted, and other people chime in with "Why are you trusting a fabulist like ChatGPT instead of going to actual resources with definitions and explanatio…

I wonder if it would create a singularity in spacetime by posting the GPT answer to "what is cunningham's law" here?

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

#165

Post by Jweb_Guru »

charcircuit wrote: post #163
Jweb_Guru wrote: post #157

Earlier quoted context omitted.

This is true but mostly meaningless in practice. I have never found the people who say this every time formal verification comes up to be the same people who actually work in formal verification. The reality is that it's far far harder to mess up a formal spec that you actually have to prove a concrete instance of, than it is to mess up the code. With a buggy spec, in the course of trying to prove it you'll arrive at…

>Formal spec bugs happen, but they're quite rare A lot of specs bugs happen all the time. If you think people can account for all edge cases in massively complex projects you are wrong. There are many behaviors that you can't predict will be nonsensical ahead of time until you actually hit them. Formal verification is not a silver bullet. Despite all of the extra effort bugs will still happen. It's better to invest i…

Can you point me to some of the concrete bugs in formal specs with associated proofs that you are thinking of? Specifically in the part that was formally verified, not in a larger project that incorporates both verified and unverified components. Because my experience is that when asked to actually provide concrete examples of how formally verified code has bugs in practice, people find it quite difficult to do so. Formal verification is about as close to a silver bullet as it gets for eliminating bugs, even if it's not 100% (nothing is). It's certainly far better at eliminating bugs than vague philosophical positions like "making things safe by default" (what does that mean?) or "abort when you're in a bad state" (how do you know you're in a "bad" state? Isn't it in general at least as difficult as figuring out what the correct formal spec is? How easy is it to detect? Is the performance cost acceptable?).

In fact, what usually happens is the opposite of a formal proof being undermined by a bad spec--when an informal spec is formally verified, inconsistencies are often found in the original spec during the course of the proof process, and bugs are subsequently found in older implementations of that spec. Fixes are then incorporated into both the original spec and the existing implementations. Formal verification is a spec-hardening process.

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

#166

Post by rey0927 »

oh_sigh wrote: post #153
rey0927 wrote: post #8

Earlier quoted context omitted.

some claim his intelligence is the highest ever measured

He's really really really good at math, but is he really really really good at a bunch of other unrelated fields too? It seems silly to imply that math skills are all there is to intelligence.

I think you don't actually know about g-factor. basically what these so called 'intelligence tests' measure is the rate at which one can absorb information and apply it abstractly, how you can come up with solutions to problems by basically doing high-level abstractions, finding patterns and connecting dots, finding things that no one thought of or came to their mind. What this means is that even though he might not know about how to do other things at first once he starts delving into them he can quickly learn them and really excel in them. What these test measure is the G factor and that if you are good at one thing you'll also be good at other things and I'm not making this up there is loads of evidence for this. the most rigorously tested idea in the field of psychology/ psychometrics is intelligence. if you had to choose one single concept out the whole field it would be intelligence. you can read the g-factor and how they measure it, all the theory, stats everything and then tell me what do you think.

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

#167

Post by aSanchezStern »

jlouis wrote: post #159
kccqzy wrote: post #135

Earlier quoted context omitted.

Formal verification is often not the best tool for ensuring code correctness from an ROI perspective. Things like unit tests (including property based tests) and ensuring 100% code coverage often achieve adequate results with less effort.

The key point is that most software don't need correctness to the level formal verification provides. There's a subset of software however, for which there's no substitute for a formal verification process.

Additionally, formal verification usability is an area of constant research, and the set of software for which it is the best ROI increases over time.

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

#169

Post by aSanchezStern »

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

Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of the initial phase of supervised learning on existing proofs to prove new ones, there's TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), and Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), among others. Most of these have some sort of language model within them, but if you're specifically looking for the LLM's that have been big recently, there's GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), and COPRA (https://arxiv.org/abs/2310.04353), though currently these models don't seem as effective as the specialized non-LLM tools. In terms of using reinforcement learning to learn beyond human written proofs, there's TacticZero (https://openreview.net/forum?id=edmYVRkYZv), this paper from OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), the HOList line of work (https://arxiv.org/pdf/1905.10006.pdf), and HyperTree Proof Search (https://arxiv.org/abs/2205.11491), as well as some in progress work I'm working on with a team at the University of Massachusetts.

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

#170

Post by turndown »

mettamage wrote: post #65
user3939382 wrote: post #60

I’m really excited about dependent types. I’m expecting we won’t get them for a while though. Dependent Haskell is progressing but apparently it’s hard to retrofit. Idris’ own creator has said he expects it to be a model for other languages, I don’t think it will ever have mainstream adoption. Coq and Agda, F* aren’t really designed to be general purpose. Although the implementation for the compiler is complex, and t…

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…

It’s simplest explanation is that dependent types are types whose exact type use some kind of parameterized value in the definition. So a dependently typed array would use a parameterized length value as part of it’s definition(this is usually the easiest example to understand). So an array of length 4(of whatever type) could be identified as different from an array of length 5, etc.
Post reply on HN