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

171–180 of 230 posts

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

#171

Post by iso8859-1 »

atomicnature wrote: post #137
aeonik wrote: post #32

Earlier quoted context omitted.

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

That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.

There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...

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

#172

Post by gtirloni »

olddustytrail wrote: post #160
gtirloni wrote: post #61

Tangent useless comment: while checking this Mastodon instance, I noticed a specific user is spamming the global feed by replying to his own posts every other day. I only saw his posts, mostly, and wondered if this was a personal instance of sorts.

Did you notice that the domain is maths tadon.xyz so it's probably a pretty small user base.

Yes, I noticed the domain and the small instance, but I missed your point.

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

#173

Post by danenania »

strikelaserclaw wrote: post #151
X6S1x6Okd1st wrote: post #138

He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people

gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.

Especially now that the training cutoff is being moved up to April 2023. Questions requiring more recent results were the main ones I’ve been going back to google for.

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

#174

Post by charcircuit »

Jweb_Guru wrote: post #165
charcircuit wrote: post #163

Earlier quoted context omitted.

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

>Specifically in the part that was formally verified

No, I am saying that is that it is easy to not verify something because you don't know the requirements up front.

>"making things safe by default" (what does that mean?)

It mean that complexity is abstracted away such that it is hard to the wrong thing.

>"abort when you're in a bad state" (how do you know you're in a "bad" state?

There are invariants which you can assume that are always true. If they aren't true for whatever reason you can abort and later track down what caused you to enter this state. It could be as simple as some logic bug or obscure as hardware malfunctioning and causing a bit flip (at scale you need to deal with hardware misbehaving).

>inconsistencies are often found in the original spec during the course of the proof process

Bugs are found in the process of testing too.

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

#175

Post by ianandrich »

0xpgm wrote: post #73

Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.

Python's Deal library provides contracts and a small portable formal proofs area of the codebase.

Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.

It just works surprisingly well for incrementally building up provable code properties.

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

#176

Post by pjmlp »

kmill wrote: post #125
tux3 wrote: post #26

Earlier quoted context omitted.

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

Yeah, here is where TLA+ fails to gain adoption, because it is only a model, how people actually implement the architecture is completely unrelated to how the model was validated.

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

#178

Post by ben_w »

dooglius wrote: post #134
ben_w wrote: post #56

Earlier quoted context omitted.

I'm sure some people do indeed say that, as that has also been said about most famous smart people. However, from my experience as someone who scored "off the charts" on a UK school Cognitive Abilities Test and 148 on an IQ test: any score over 130 is suspect, as basically nobody is collecting enough data to make the tests statistically valid once you're more than 2σ from the mean.

What do you mean by statistically valid? Are you just saying that the map between the raw scores and a z-score is questionable (and thus comparing scores between different tests is invalid), or are you making a deeper claim?

Both, I think. However I would also add that my understanding is second-hand, reading and watching what others have to say rather than any deep academic research of my own.

Every source I've read or watched all agree the sample sizes used when creating the tests in the first place just aren't large enough to be all that confident beyond 2σ.

There's also the problem that training on tests is effective, which limits the ability of a test to be validated on those taking it fairly soon after it gets published.

A further other issue is that most IQ tests pre-suppose the existence of a G-factor and treat differences between types of intelligence as noise rather than a signal for the existence of any multi-factor variation. I don't know which hypothesis is correct (I lean towards thinking it's mostly a G-factor, but there are clearly some things which can only be explained by multi-factor models, e.g. where a skill is entirely absent such as in the case of dyscalculia).

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

#179

Post by oh_sigh »

rey0927 wrote: post #166
oh_sigh wrote: post #153

Earlier quoted context omitted.

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…

I'm familiar with g-factor.

But why is it that the people who always score the highest on IQ tests contribute the most to math, and only a little bit to all the other subjects under the sun?

Why aren't they also creating the greatest art, growing the greatest vegetables, and, I don't know, designing the greatest structural engineering designs in the world?

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

#180

Post by alexisread »

speed_spread wrote: post #48
rey0927 wrote: post #8

Earlier quoted context omitted.

some claim his intelligence is the highest ever measured

He's gonna fix EVERYTHING. And he's gonna do it in ONE WEEK!

For those that don't get the reference, president Camacho from Idiocracy :)
Post reply on HN