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

111–120 of 230 posts

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

#111

Post by samvher »

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…

I had the same positive experience with Software Foundations.

There is another book somewhat derived from it (if I understand correctly) using Agda instead of Coq: https://plfa.github.io/

I haven't had the chance to go through it yet, but it's on my list - I think Agda (and as mentioned by another commenter, Idris) is likely to feel more like a programming language than Coq.

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

#112

Post by jyunwai »

yodsanklai wrote: post #107
c7b wrote: post #6

Earlier quoted context omitted.

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

What would make him greater than other fields laureate?

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.

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

#113

Post by Jtsummers »

mettamage wrote: post #110
xeonmc wrote: post #97

Earlier quoted context omitted.

ChatGPT = Cunningham bait

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 explanations that aren't garbage? Here's what it actually is..."

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

#114

Post by malwrar »

chx wrote: post #14
SushiHippie wrote: post #3

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

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

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

#115

Post by skulk »

valyagolev wrote: post #109
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…

I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program. If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have every…

Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.

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

#116

Post by omginternets »

btreecat wrote: post #72
j7ake wrote: post #39

Earlier quoted context omitted.

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

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

Lack of culture on your part?

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

#117

Post by omginternets »

LoganDark wrote: post #104
hiddencost wrote: post #89

Earlier quoted context omitted.

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

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

Welcome! You now know who Terence Tao is :)

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

#119

Post by svat »

julianeon wrote: post #82
opan wrote: post #58

Earlier quoted context omitted.

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

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

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

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

#120

Post by snovv_crash »

mrkeen wrote: post #35
mjburgess wrote: post #16

Earlier quoted context omitted.

The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. Certain sorts of algorithmically complex development (games, cars, medical hardware, etc.) would benefit from a 'closed-world verification' -- but that's not most software, and they have alternatives. 'Code correctness', including unit testing, ends up being…

Strong disagree. > The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. The choice to run a system as many different moving parts is a decision taken by the team in order to avoid failure . > Certain sorts of algorithmically complex development -- but that's not most software It's all software. > 'Code correctn…

Tests only show that it is correct for the sets of values and code paths you exercise. It's quite possible for other aspects to be incorrect, and this is what theorem provers like Coq help with.
Post reply on HN