Tangent useless comment: while checking this Mastodon instance, I noticed a specific user is spamming the global feed by replying to his own posts every other day. I only saw his posts, mostly, and wondered if this was a personal instance of sorts.
Lean4 helped Terence Tao discover a small bug in his recent paper
61–70 of 230 posts
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#62Earlier quoted context omitted.
Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.
the missing context from the previous comment is that Tao used GitHub Copilot to help with learning Lean. He's been writing about it as he goes, most recently: https://mathstodon.xyz/@tao/111271244206606941
Thanks for adding the clarification. I thought this was more common knowledge. I will update my comment accordingly.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#63Earlier quoted context omitted.
If mathematicians have "a good instinct" does that suggest that their brains can somehow apply an informal proof? I wonder if they are good, or if it's selection/confirmation/other biases that lead is to think say. Also, aren't surprising results the most interesting!?
In an informal sense disproving things is easier than proving things. For example theorems often say thing like "all objects of type Y have property X", its very difficult to work out even where to start proving such a statement unless you're an expert in Y and X, but to disprove it all you have to do is find some example Y which doesn't have property X. If you've worked with Y things for a while you probably have a…
> In an informal sense disproving things is easier than proving things.
Note that this is not true in general, and depends on the type of theorem. The idea is that while it’s easy to show why a particular proof is incorrect, it’s much more difficult to show that every proof is incorrect.
Formally, this idea is captured by CoNP, which is believed to be different from NP and hence a strict superset of P.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#64If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem…
Anyway, check out Idris[2], it’s cool for this sort of thing
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#65I’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 operations respect this length. This makes it possible to catch certain kinds of errors before the code even runs.
For example, in a language with dependent types, you could specify a function to take a list of length 3 and no other sizes. If you tried to pass a list of length 4, the program wouldn't compile, preventing this kind of mistake early on.
It's a bit like having an extra layer of safety checks, where the types are more expressive and can encode more intricate relationships between variables.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#66Does anyone understand what the proof is about? An improved boundary on the mean of geometric series? And why it's only a problem for n=3, k=2, and not for all k=n-1?
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#67Earlier quoted context omitted.
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.
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.
in france the age if you follow the traditional scholl schedule to have a phd is 26.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#68Earlier quoted context omitted.
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…
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…
> 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.
A reminder of Gall's law:
> A complex system that works is invariably found to have evolved from a simple system that worked. A complex system designed from scratch never works and cannot be patched up to make it work. You have to start over with a working simple system.[8]
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#69I’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…
Another classic use case is that you can have expressions in the types of your function, for example this won't compile:
stringOrInt : (x : boolean) -> int -> (if x then String else int)
stringOrInt true x = toString x
stringOrInt false x = x + 1
1 + stringOrInt true 37 # this will error, because it knows you've not returned an int
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#70For 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…
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...
Famous photo of him studying with Paul Erdős at age 10: https://i0.wp.com/blogs.ams.org/blogonmathblogs/files/2015/0...
