[SushiHippie]

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 Carol Collins chair.

https://en.wikipedia.org/wiki/Terence_Tao

[j7ake]

Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.

[jvm___]

If you're going for a PhD or researching some obscure, furthest reach study of some mathematical principle and you get stuck. One of the ways to move forward is to hope that Terence Tao finds your topic interesting and can give you a few minutes of his time - because he'll probably have some ideas for moving your research forward.

[daynthelife]

Conversely, there’s a running joke that you’re in big trouble if Terry Tao takes too much of an interest in your topic of study, since he will inevitably solve all but the hardest problems in the field.

[benibela]

I got stuck solving a polynomial equation system for years

Perhaps I should try sending him a mail

[btreecat]

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

[andrewflnr]

You can't expect the entire Internet to always provide enough context for you personally, with your exact level of knowledge, to understand a social media post with no additional effort. How do you expect that to work at scale? Meanwhile, Google is just a tab away.

[thornewolf]

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

[swatcoder]

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.

[ndsipa_pomu]

I don't have much interest in celebrity either, but I feel that you're short-changing Terence Tao. He's not really famous due to being celebrated, but he's celebrated due to his level of skill and breadth of mathematical knowledge (sometimes known as the Mozart of Mathematics).

I think your sentiment is misplaced as I would expect HN commenters to have heard of Tao as he often features in posts about mathematics. I'm sure I recall seeing some comments from him too.

There's an approachable Numberphile video featuring him here: https://www.numberphile.com/videos/the-worlds-best-mathemati...

[VirusNewbie]

I started to agree with you, but let's keep in mind that there are new generations of tech geeks out here who are just learning about the things we live and breathe.

[fifilura]

I am sure 100% of thornewolf and 99% of people reading the same news as you know who Terence Tao is, but extrapolating from your own perspective is treacherous.

https://xkcd.com/1053/

[LoganDark]

https://xkcd.com/2501

[hiddencost]

Yes. Not knowing who Terry Tao is,, if you're on HN, makes you an outlier.

[LoganDark]

Hi, it's me, I'm the outlier, it's me

[omginternets]

Welcome! You now know who Terence Tao is :)

[wholinator2]

Not any more

[pfdietz]

Congratulations! You're one of today's lucky 10,000.

https://xkcd.com/1053/

[omginternets]

Lack of culture on your part?

[c7b]

It's correct that he is a professor at UCLA, but it's also worth mentioning that he's regularly called nicknames like 'greatest mathematician alive' (just try googling that phrase): https://academicinfluence.com/rankings/people/most-influenti...

[meowface]

Famous photo of him studying with Paul Erdős at age 10: https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/0...

[yodsanklai]

What would make him greater than other fields laureate?

[jyunwai]

Beyond the incredible quality and quantity of his work starting from early in his life, what makes Terence Tao memorable to me, is his approachability and willingness to write advice for mathematicians and math students in a blog: https://terrytao.wordpress.com/career-advice/

He also has an active Mastodon, which further makes him more approachable: https://mathstodon.xyz/@tao

It's rare to see a professional at the top of an academic field remain so encouraging to other people in the field, and work to make their work accessible to colleagues across different levels of mathematical maturity.

[ndsipa_pomu]

Other mathematicians opinions of him and his work. He's very prolific and was considered a child prodigy.

[chx]

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.

[pjmlp]

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.

[n4r9]

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.

[alliao]

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

[n4r9]

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

[poulpy123]

in france the age if you follow the traditional scholl schedule to have a phd is 26.

[NotYourLawyer]

Yeah but since he did all this in the USA, I’m not sure why that’s relevant.

[pjmlp]

It isn't, I was making the point university degrees aren't the same everywhere.

[malwrar]

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 ensure they got at least 4 years of tuition out of me. I’ve always wondered how people somehow managed to speedrun to the top like this, rather than just being bored by their classes (esp gen-ed classes ugh) until they reach top rank the normal way.

[waythenewsgoes]

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.

[dllthomas]

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.

[Scaless]

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.

[chx]

In the 90s I sort of attended two universities at the same time in Hungary (given the time and the place it's not as big a deal as it sounds) and I said to the second one, hey I know the basic stuff, let me attend the more advanced one and they said, sure, no skin off my back, do whatever you want, if you fail, that's a you problem but if you pass the more advanced tests we will credit you the basic stuff.

[pas]

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)

[JonChesterfield]

Youtube has forgotten what "audio" is for me so noting the first talk is also at https://www.microsoft.com/en-us/research/video/the-future-of... - which is using youtube - but manages to make noises. Which I suppose is a pointwise instance arguing that software does not work as well as it might do.

[opan]

I'm relieved that Lean4 doesn't seem to be some AI thing.

[julianeon]

Now that you mention it, Tao did say he used ChatGPT to help teach himself Lean.

https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...

[svat]

Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao

He's been posting about it since Oct 9: https://mathstodon.xyz/@tao/111206761117553482

> I have decided to finally get acquainted with the #Lean4 interactive proof system (using AI assistance as necessary to help me use it), as I now have a sample result (in the theory of inequalities of finitely many real variables) which I recently completed (and which will be on the arXiv shortly), which should hopefully be fairly straightforward to formalize. I plan to journal here my learning process, starting as someone who has not written a single line of Lean code before.

There are several posts mentioning how GPT has been useful (though not always) at suggesting things, including one linking to this transcript with ChatGPT: https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a...

[sebzim4500]

There is a project to connect GPT-4 and lean, but I doubt they will make a lot of progress until they can finetune GPT-4.

https://www.youtube.com/watch?v=CEwRMT0GpKo

[zozbot234]

Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.

[alexvitkov]

Things usually stop being considered as AI when they start working.

[rprenger]

You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 (shameless plug)

[antonioevans]

Field's Medal winner.

[sriram_sun]

nit: Fields Medal (no apostrophe).

[jagrsw]

> where he holds the James and Carol Collins chair

What is the academic impact of holding an endowed chair like the 'James and Carol Collins chair'? It it related to any specific advantages or responsibilities? Those titles seem like they serve as a form of recognition for donors, is there a deeper significance behind them?

[chongli]

The advantage is that the chair usually comes with a bunch of money which you can use to fund grad students and pay for research. The latter is of course much more important in experimental sciences and engineering than it is in math. Still, mathematicians often do hire grad students to do grunt work for them.

[tnecniv]

Often, no, but some are particularly prestigious due to the lineage of individuals who had held the chair. Others have some special requirements like any endowment. Mostly, it is not really meaningful though.

[rey0927]

some claim his intelligence is the highest ever measured

[ben_w]

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.

[dooglius]

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?

[ben_w]

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

[throw_pm23]

He's a great mathematician all right, but that is a very silly way to put it.

[speed_spread]

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

[alexisread]

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

[rey0927]

if he helps in building AGI then yes

[readyplayernull]

You know, we have this thing in our company, when someone performs so well they can do other people's work.

[oh_sigh]

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.

[rey0927]

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.

[oh_sigh]

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?

[rey0927]

>greatest art

first, tell how one measures art

>greatest vegetables

If he does work in the field of animal/plant genetics I am hopeful he will discover great things and move the field forward

>structural engineering

again this is not what he does, and why he does math is.....i don't know what's his reason to do math, idk his motivations behind it but i do surely believe there are high-iq structural engineers out there of course they are how can you say there are none. greatest structural engineering designs made yet are actually made by geniuses or highly intelligent people you wouldn't expect a kid who fails high school to make those things do you?