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

131–140 of 230 posts

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

#131

Post by dllthomas »

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…

It wasn't "like this" but I just (with parental support) enrolled in the local community college after junior high, took a light load of college work, and got a homeschool program to sign off until I could test out at 16. Did 2 years worth of college work over the 4 years that would have been highschool, then transferred to a "proper" university as a junior at 18.

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

#132

Post by n4r9 »

alliao wrote: post #41
n4r9 wrote: post #40

Earlier quoted context omitted.

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.

I'm sure you're remarkable enough congratulations for your hard work

Not remarkable enough to land a post doc and stay in academia. But thank you :)

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

#133

Post by swatcoder »

thornewolf wrote: post #90
btreecat wrote: post #72

Earlier quoted context omitted.

So that's an excuse for such a low context post?

For the HN crowd, explaining who Terrence Tao is would be ike explaining who Obama is

This may be hard to believe, but a lot of us here in "the HN crowd" have zero interest in celebrity and do not keep a catalog of them all in our heads. Even intellectual ones. There's nothing wrong with that, but it's also just its own interest one or may not have.

People approach things in a lot of different ways and it would be nice if we can just respect that instead of digging on each other or making unfounded assumptions.

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

#134

Post by dooglius »

ben_w wrote: post #56
rey0927 wrote: post #8

Earlier quoted context omitted.

some claim his intelligence is the highest ever measured

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?

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

#135

Post by kccqzy »

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…

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.

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

#136

Post by drdeca »

Ar-Curunir wrote: post #63
eigenket wrote: post #37

Earlier quoted context omitted.

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…

> In an informal sense disproving things is easier than proving things. Note that this is not true in general, and depends on the type of theorem. The idea is that while it’s easy to show why a particular proof is incorrect, it’s much more difficult to show that every proof is incorrect. Formally, this idea is captured by CoNP, which is believed to be different from NP and hence a strict superset of P.

> which is believed to be different from NP and hence a strict superset of P

“a strict superset of P” doesn’t really follow from that. P is also believed to be different from NP, and P is certainly not a strict superset of P.

Of course, I assume you just misspoke slightly, and that whatever it is that you actually meant to say, is correct.

E.g. maybe you meant to say “coNP is believed to both be strict superset of P (as is also believed about NP), and distinct from NP.”

I think it is believed that the intersection of NP and coNP is also a strict superset of P, but that this is believed with less confidence than that NP and coNP are distinct?

I imagine I’m not telling you anything you don’t already know, but for some reason I wrote the following parenthetical, and I’d rather leave it in this comment than delete it.

(If P=NP, then, as P=coP, then NP=P=coP=coNP , but this is considered unlikely.

It is also possible (in the sense of “no-one has yet found a way to prove otherwise” that coNP = NP without them being equal to P.

As a separate alternative, it is also possible (in the same sense) that they are distinct, but that their intersection is equal to P.

So, the possibilities: P=NP=coNP, P≠cocapNP=NP=coNP, P=cocapNP≠NP,coNP, All 4 are different, (cocapNP is the intersection of NP and coNP)

Where the last of these is I think considered most likely? )

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

#137

Post by atomicnature »

aeonik wrote: post #32
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

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

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

#138

Post by X6S1x6Okd1st »

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

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

#139

Post by mensetmanusman »

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

I have found that good communicators that don’t code can quickly make functional automation.

Interestingly, LLMs may end up contributing to more inequality if only the highly skilled can leverage them effectively.

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

#140

Post by valyagolev »

skulk wrote: post #129
valyagolev wrote: post #121

Earlier quoted context omitted.

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

i don't even need it to go beyond the insides of a function. something like a proof of an invariant that's only relevant inside the function's body would be fine. e.g. in Rust, almost every place where you see something like ".unwrap()" with "// unwrap safety:" comment, this comment could be an assertion easily proven from the few lines above
Post reply on HN