10 ms·

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

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/ 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 https://en.wikipedia.org/wiki/Terence_Tao

deleted 3y ago
[deleted]
antonioevans 3y ago
Field's Medal winner.
- sriram_sun 3y ago
  nit: Fields Medal (no apostrophe).
c7b 3y ago
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-influential-mathematicians-today https://academicinfluence.com/rankings/people/most-influenti...
- yodsanklai 3y ago
  What would make him greater than other fields laureate?
  - jyunwai 3y ago
    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/ https://terrytao.wordpress.com/career-advice/ He also has an active Mastodon, which further makes him more approachable: https://mathstodon.xyz/@tao 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 3y ago
    Other mathematicians opinions of him and his work. He's very prolific and was considered a child prodigy.
- meowface 3y ago
  Famous photo of him studying with Paul Erdős at age 10: https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/09/Paul_Erdos_with_Terence_Tao.jpg https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/0...
rey0927 3y ago
some claim his intelligence is the highest ever measured
- oh_sigh 3y ago
  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 3y ago
    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 3y ago
      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 3y ago
        >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?
chx 3y ago
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.
- malwrar 3y ago
  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 3y ago
    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.
  - Scaless 3y ago
    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.
pas 3y ago
Kevin Buzzard (a professional mathematician) has a few good talks about Lean https://youtu.be/Dp-mQ3HxgDE https://youtu.be/Dp-mQ3HxgDE from 2019 at MS Research https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s (2022 at ICM international math congress)
- JonChesterfield 3y ago
  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-mathematics/ 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.
j7ake 3y ago
Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.
- jvm___ 3y ago
  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.
  - benibela 3y ago
    I got stuck solving a polynomial equation system for years Perhaps I should try sending him a mail
  - daynthelife 3y ago
    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.
- btreecat 3y ago
  So that's an excuse for such a low context post?
  - omginternets 3y ago
    Lack of culture on your part?
  - hiddencost 3y ago
    Yes. Not knowing who Terry Tao is,, if you're on HN, makes you an outlier.
    - LoganDark 3y ago
opan 3y ago
I'm relieved that Lean4 doesn't seem to be some AI thing.
- sebzim4500 3y ago
  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 https://www.youtube.com/watch?v=CEwRMT0GpKo
- zozbot234 3y ago
  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.
  - rprenger 3y ago
    You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 (shameless plug)
  - alexvitkov 3y ago
    Things usually stop being considered as AI when they start working.
- julianeon 3y ago
  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=4jd61tn6MlpOFUFSrupxWg https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...
  - svat 3y ago
    Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao He's been posting about it since Oct 9: https://mathstodon.xyz/@tao/111206761117553482 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-55f15a2bd871 https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a...
jagrsw 3y ago
> 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?
- krsrhe 3y ago
  [dead]
- tnecniv 3y ago
  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.
- chongli 3y ago
  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.

deleted 3y ago

[deleted]

antonioevans 3y ago

Field's Medal winner.

sriram_sun 3y ago
nit: Fields Medal (no apostrophe).

c7b 3y ago

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-influential-mathematicians-today https://academicinfluence.com/rankings/people/most-influenti...

yodsanklai 3y ago
What would make him greater than other fields laureate?
- jyunwai 3y ago
  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/ https://terrytao.wordpress.com/career-advice/ He also has an active Mastodon, which further makes him more approachable: https://mathstodon.xyz/@tao 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 3y ago
  Other mathematicians opinions of him and his work. He's very prolific and was considered a child prodigy.
meowface 3y ago
Famous photo of him studying with Paul Erdős at age 10: https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/09/Paul_Erdos_with_Terence_Tao.jpg https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/0...

rey0927 3y ago

some claim his intelligence is the highest ever measured

oh_sigh 3y ago
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 3y ago
  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 3y ago
    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 3y ago
      >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?

chx 3y ago

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.

malwrar 3y ago
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 3y ago
  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.
- Scaless 3y ago
  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.

pas 3y ago

Kevin Buzzard (a professional mathematician) has a few good talks about Lean https://youtu.be/Dp-mQ3HxgDE https://youtu.be/Dp-mQ3HxgDE from 2019 at MS Research https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s (2022 at ICM international math congress)

JonChesterfield 3y ago
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-mathematics/ 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.

j7ake 3y ago

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

jvm___ 3y ago
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.
- benibela 3y ago
  I got stuck solving a polynomial equation system for years Perhaps I should try sending him a mail
- daynthelife 3y ago
  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.
btreecat 3y ago
So that's an excuse for such a low context post?
- omginternets 3y ago
  Lack of culture on your part?
- hiddencost 3y ago
  Yes. Not knowing who Terry Tao is,, if you're on HN, makes you an outlier.
  - LoganDark 3y ago

opan 3y ago

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

sebzim4500 3y ago
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 https://www.youtube.com/watch?v=CEwRMT0GpKo
zozbot234 3y ago
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.
- rprenger 3y ago
  You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 (shameless plug)
- alexvitkov 3y ago
  Things usually stop being considered as AI when they start working.
julianeon 3y ago
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=4jd61tn6MlpOFUFSrupxWg https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...
- svat 3y ago
  Instead of a twitter post of screenshots of it, the direct link to Tao's Mathstodon is: https://mathstodon.xyz/@tao https://mathstodon.xyz/@tao He's been posting about it since Oct 9: https://mathstodon.xyz/@tao/111206761117553482 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-55f15a2bd871 https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a...

jagrsw 3y ago

> 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?

krsrhe 3y ago
[dead]
tnecniv 3y ago
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.
chongli 3y ago
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.