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

91–100 of 230 posts

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

#91

Post by daynthelife »

jvm___ wrote: post #71
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.

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.

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.

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

#92

Post by chongli »

jagrsw wrote: post #84
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…

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

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.

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

#93

Post by howenterprisey »

mettamage wrote: post #65
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…

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that o…

I never care much for chatgpt answers. I don't know why people post them on here.

In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason.

The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fair, those examples are technically dependent types, but it would be better to give an example that's impossible in those languages, such as "array with length at most 3" or "even integer".

Finally, to nitpick, "a bit like" is unneeded hedging.

Stack Overflow did a much better job: https://stackoverflow.com/questions/9338709/what-is-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.

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

#94

Post by alexvitkov »

zozbot234 wrote: post #80
opan wrote: post #58

Earlier quoted context omitted.

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

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.

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

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

#95

Post by woolion »

throwalean wrote: post #24
woolion wrote: post #19

Earlier quoted context omitted.

"Terry Tao finds ChatGPT very helpful to prove new theorems" would actually be bigger news than this one, IMO.

"Terry Tao finds ChatGPT very helpful to formally verify his new theorems" seems to be a true statement. See some of his other recent mathstodon toots.

The point is that LLMs and similar tools tend to be very good at automating the trifle but not very useful at what would be considered really "interesting" work.

So while your point is somewhat true [0], as he mentions that these tools could become good enough to do the formal verification part, it's precisely not the interesting part. See [1] and [2]; in particular some things that are very easy to do in real maths can be very challenging in an automated theorem prover, quoting from [2]:

>In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation [...]

It's impressive to be able to do such mathematics in Lean/Coq..; at all, but it is very tedious mechanical work [3].

>It was more tedious than I expected, with each line of proof taking about an hour to formalize

So I think that rather proves the point of what LLMs are currently good for, and what tools can help for really difficult tasks, rather than invalidate it.

[0] https://mathstodon.xyz/@tao/111305365372766606

[1] https://mathstodon.xyz/@tao/111305336701455719

[2] https://mathstodon.xyz/@tao/111259986983504485

[3] https://mathstodon.xyz/@tao/111305336701455719

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

#96

Post by andrewflnr »

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?

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.

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

#97

Post by xeonmc »

howenterprisey wrote: post #93
mettamage wrote: post #65

Earlier quoted context omitted.

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that o…

I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fai…

ChatGPT = Cunningham bait

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

#98

Post by howenterprisey »

xeonmc wrote: post #97
howenterprisey wrote: post #93

Earlier quoted context omitted.

I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fai…

ChatGPT = Cunningham bait

Worked for me :<

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

#99

Post by krsrhe »

jagrsw wrote: post #84
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…

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

[dead]

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

#100

Post by krsrhe »

tux3 wrote: post #26
ohduran wrote: post #17

Earlier quoted context omitted.

Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison? Edit: Wrote Allow the first time, good stuff.

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…

Lean is for verifying proofs, not writing them. It helps you find mistakes, but doesn’t help you understand or express ideas in a human readable way.
Post reply on HN