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

Post by gmadsen » Fri, Oct 27, 2023, 12:59 PM UTC

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…

Post by passion__desire » Fri, Oct 27, 2023, 1:06 PM UTC

omneity wrote: post #47

That one of the brightest minds of our generation is able to increase his bandwidth with the combination of LLMs and automated proofs makes me super bullish on this tech combo in the future! It starts with bug-fixing, then supports verification, until it starts propelling new discoveries and push the envelope. We need a term when a dynamic like Moore's Law "infects" a field that had no such compounding properties bef…

Post by NotYourLawyer » Fri, Oct 27, 2023, 1:09 PM UTC

pjmlp wrote: post #20

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.

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.

Post by tnecniv » Fri, Oct 27, 2023, 1:18 PM UTC

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?

Post by hiddencost » Fri, Oct 27, 2023, 1:31 PM UTC

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?