Lean4 helped Terence Tao discover a small bug in his recent paper
mathstodon.xyz
mathstodon.xyz
https://mathstodon.xyz/@tao/111208692505811257
Many of his mastodon posts this month have been about his learning progress.
Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
Interestingly, LLMs may end up contributing to more inequality if only the highly skilled can leverage them effectively.
I (having 30 years experience as a professional Software Developer^TM) am begging him to teach me his techniques.
Now that you mention it, I met him and we became friends in large part due to his communications abilities.
Phind is often recommended to me by programmers who find it produces "better" results than a naive GPT-4 session, but I don't know that anyone has done any real world testing.
I understand your skepticism (because the internet is fully broken right now/and forum posts are more or less paid for content at this point)
but...its a bit funny you'd like someone who just explained they're a beginning programmer who got into programming because an LLM helped remove insane amounts of friction from the learning process to "explain a mechanism" to them.
However, over time, the overwhelming benefits of using LLMs will be well understood, and these ladder climbers will absolutely master LLMs, no matter their intelligence. People can become experts at taking exams despite how boring and soul sucking that can be, let alone using something way funner and useful like LLMs.
For any relatively simple task I can say "Write a Python script to do X" and it will almost always spit out working code, even if it has subtle mistakes. Fixing mistakes is fine and part of the process. I don't have to read StackOverflow posts saying "Do you really want to do X?", or sift through documentation that follows the author's approach of how they want to introduce the material but doesn't directly address my question.
GPT would be good as a search engine, but who would want a search engine that stopped indexing a few years back? Also, it is not good at ultra niche topics, which would be the whole point of a search engine.
To me, the first one is the most basic and frankly, most silly definition of a 10x programmer - produces more code? really? Code sucks. Nobody needs more code, people need solutions. Solving a problem with no more code, or understanding it so a _tiny_ change solves all problems? Way better than adding code, actually much harder to synthesize and produce new results. Way more efficient.
Now can you remove things and solve the problem? Realize you can build an even more simple and generic system that solves your problem? Even more amazing.
More code per unit of time, not necessarily more code in an absolute sense.
The latter would be a bad thing.
Like if the answer is not a leetcode/CRUD code sample you can easily find on the internet either way, it can’t do anything useful. Like, my problems mostly constitute things like reasoning about the correctness of a given change in the context of the whole codebase, its threading model, etc. It will at best regurgitate some bullshit like “race conditions can be this and that” here, not helping at all.
And if you just want to read without playing a game: https://lean-lang.org/theorem_proving_in_lean4/introduction....
Edit: Wrote Allow the first time, good stuff.
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 verified math that people can contribute to and use in new proofs.
A big multi-year effort to start formalizing the proof of Fermat's Last Theorem in Lean 4 was approved recently: https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/AITP_2022_F...
A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).
There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )
Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )
And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )
Do you have to actually prove a tactic work for it to be sound? A tactic will rewrite the program into a simplified program that will verified by a kernel; if the tactic wrongly expands something, the kernel will later reject the program. Only the itself kernel need to be verified for the whole thing to be sound.
Or am I missing something?
Do correct me if I’m wrong, but Lean is more about total functions/FP code, not sure how well does it handle threading, if at all. It might be more related to the correctness of the actual implementation of a serial algorithm.
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 book are little games and I found them quite enjoyable to work through.
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/microsoft/CodeContracts
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 a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end.
The effort to source-level-check source-level-code is largely a huge waste of time and creates an illusion of reliability which rarely exists.
> 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 correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end.
No and no. I have comprehensive end-to-end tests. They take forever, don't fit into RAM (for some services I need to run them on my home PC because my work laptop only has 16GB), and most importantly: they show that the code is not correct. Now I have to change incorrect code to correct code (while not breaking any public interfaces. I wish my predecessors did not put incorrect code into the live system.
My claim is that these techniques help in relatively few areas of software development. In the main, software is built with open-world interactions across a range of devices (network, disk, etc.) where those interactions dominate the net failure modes of the system.
In the latter case, source-level verification is not only of no help, but it's a huge resource misallocation. You end up writing tests that just create the illusion of success; and then the whole thing constantly falls over.
Spend all that time instead in designing tests that do fit into ram (eg., sample your datasets); and instrumentation that does reveal errors (eg., sampling of memory, requests, etc.).
One of my first software jobs was writing a reverse proxy -- one of my co-devs wrote unit tests that simply established the in/out of various functions was "as expected". Pretty useless -- the issue is whether the proxy actually worked.
Likewise most source-level correctness efforts are 'testing theatre'.
Devs are looking for cargo-cult solutions they can copy/paste. No, testing software is an actual area of development -- and you need to develop tests, not cargo-cult
A lot of specs bugs happen all the time. If you think people can account for all edge cases in massively complex projects you are wrong. There are many behaviors that you can't predict will be nonsensical ahead of time until you actually hit them.
Formal verification is not a silver bullet. Despite all of the extra effort bugs will still happen. It's better to invest in making things safe by default, or by aborting when getting into a bad state.
In fact, what usually happens is the opposite of a formal proof being undermined by a bad spec--when an informal spec is formally verified, inconsistencies are often found in the original spec during the course of the proof process, and bugs are subsequently found in older implementations of that spec. Fixes are then incorporated into both the original spec and the existing implementations. Formal verification is a spec-hardening process.
No, I am saying that is that it is easy to not verify something because you don't know the requirements up front.
>"making things safe by default" (what does that mean?)
It mean that complexity is abstracted away such that it is hard to the wrong thing.
>"abort when you're in a bad state" (how do you know you're in a "bad" state?
There are invariants which you can assume that are always true. If they aren't true for whatever reason you can abort and later track down what caused you to enter this state. It could be as simple as some logic bug or obscure as hardware malfunctioning and causing a bit flip (at scale you need to deal with hardware misbehaving).
>inconsistencies are often found in the original spec during the course of the proof process
Bugs are found in the process of testing too.
Granted, but "this spec doesn't attempt to cover [X]" is very different from "this spec claims to cover [X] but actually doesn't, in ways the authors are unaware of." The former is quite common in formal specs with machine-verified correctness proofs and I've never heard anyone call that a "spec bug". The latter is not common in them at all. Perhaps you didn't intend this yourself, but the way people generally talk about "there could be a bug in the spec" is usually used to imply that the latter case happens often enough to make formal verification comparably effective to other defense mechanisms, when empirically formal verification is far, far more effective than any other bug prevention mechanism--to the point that people struggle to find even individual examples of these kinds of spec bugs.
> There are invariants which you can assume that are always true. If they aren't true for whatever reason you can abort and later track down what caused you to enter this state. It could be as simple as some logic bug or obscure as hardware malfunctioning and causing a bit flip (at scale you need to deal with hardware misbehaving).
Yes, and stating these invariants precisely is generally exactly what you need to do as part of writing the formal spec; getting them right is equally hard in both cases, so it seems weird to me to say that it's easier to check the invariants at runtime than to get the spec right. In fact, many formal specs have invariants that are exactly of the form "assert that if I ran this line of code, it would not throw an exception." Moreover, you can use much more "expensive" invariants when you're creating a spec, since you don't actually have to check them at runtime, which in practice lets you catch far more and more subtle bad states than you can with software checks. For example, your proof state can include a full history of every action taken by the application in any thread, and prove that invariants on them are maintained during every instruction, even when those instructions proceed concurrently and might witness partial or stale views of the latest values in memory; storing and checking all of this information on every step on an actual machine would be wholly impractical, even for high level languages and non-performance-critical software.
Obviously, things are defined according to some base model of the world, so if you are concerned about hardware bit flips (which in rare contexts you are) your spec should take that into account, but the vast majority of bugs in modern applications are not bugs of this form, and most defensive runtime checks are equally susceptible to hardware issues or other unexpected environment changes.
> Bugs are found in the process of testing too.
Yes, and I never said testing was bad. Formal verification and testing are complementary techniques, and tests are important in a formal verification context because you should be able to prove the tests will pass if you've gotten your spec right. However, them being complementary techniques doesn't mean that they are equally effective at reducing bugs.
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]
Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138
No, it really isn't. It's doing better now than it ever has... and I mean all the negative implications of that. It was not an art that was ever "found" in the sense you mean.
Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving.
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.
Although the implementation for the compiler is complex, and the syntax can get complex and verbose, to me my requirement is simple: I want to encode everything about input and output that I know.
Right now in mainstream languages I often know more about my arguments or output than the type system will allow me to specify.
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.
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
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.
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..."
Since I guess we’re doing dependent types explanations I’ll give it a go. Dependent types extend a type system with two new type thingies: 2-tuples where the type of the second element depends on the value of the first, and functions where the type of the function’s return value depends on the value that was passed to it.
> Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".
So now you know why I do it. Also, I believe this is my first time doing it. I might be wrong.
Is it better to ask and wait for an answer instead?
There is nothing in the guidelines on HN about it. I don’t know what’s reasonable and I haven’t seen strong cultural norms from HN yet. I at least labeled that the text was from chatgpt as to not confuse it was my own text.
It all has trade offs.
However, I wouldn't recommend posting the result here if you don't know if it's correct. Moreover, anyone can ask chatgpt themselves. It's better to wait for someone here to post an answer.
Yes, there's nothing in the guidelines, but they're (deliberately) not all-encompassing. Besides, I would hope it's part of basic Internet etiquette; just because we now have access to tools that generate plausible-sounding but not necessarily correct answers to questions doesn't mean we need to post what they create in the place of genuine answers.
Yea that got lost on me. I think I view these things a bit differently than most on HN. I've noticed in general that the more I'm not at uni, the more my thinking has become heuristic and quick-ish. It used to be more thorough and in-depth. The trade-off of it being that such type of thinking is more time consuming but the answer is more comprehensive and/or accurate.
No, around here it's better to say "So dependent types are pretty much $SOMETHING_COMPLETLY_WRONG ?" and wait for all the "corrections" (aka Cunningham's law someone linked to nearby).
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 everything proven everywhere...
What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing
This doesn't even exist in TypeScript. If I change
function foo(a: any) { return baz(a); }
function foo(a: number) { return baz(a); }
Is that what you're after, asserting a dependent type? For example being able to change:
function divByTwo(a: number): number { return a/2; }
function divByTwo(a: even_number): number { return a/2; }
You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).
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 before.
EDIT:
There's additional context that Terence Tao is using Copilot to help him learn Lean. As shared by adbachman: https://mathstodon.xyz/@tao/111271244206606941
Could Terence have done it without Copilot? Sure, but like many of us he might not have initiated it due to the friction of adopting a new tool. I think LLM tech has great potential for this "bicycle for the mind" kind of scenarios.
He's been writing about it as he goes, most recently: https://mathstodon.xyz/@tao/111271244206606941
I didnt make the front page of Hacker News, of course. lol
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
The Lean proof checker could be used to automatically verify whether the synthetic proofs written by the language model are correct. This information could be used to provide an RL reward signal applied to the original language model, which would result in it writing better proofs. (Or we train a new model using the correct synthetic proofs of the previous round as training data.) And then the process repeats. So the model would self-train using its synthetic training data, without further human intervention.
We could even make this process more adversarial. First we split the generator language model into two: One which generates conjectures, and one which tries to prove/disprove them in Lean. Then add a predictor model which tries to predict whether a synthetic proof is verified by the Lean proof checker. The lower the predicted probability that the proof will be correct, the more reward gets the proof-generator model if it did indeed provide a correct proof.
Finally, we add another model which tries to predict the reward the proof-generator model will get for a given synthetic conjecture. Then the conjecture-generator model is rewarded for conjectures that are predicted to yield a high reward in the proof-generator model. So conjectures that are neither too hard not too easy for the proof-generator model.
So we would expect that the whole system would progressively create harder and harder synthetic proofs, which in turn allows for better and better self-training of the proof-generator.
It seems this could in principle scale to superhuman ability in generating proofs. The process would be somewhat similar GANs or to self-play in AlphaGo Zero.
I think the hard part is the initial bootstrapping part, to get the whole process off the ground. Because the initial training of the generator models has to be done with human provided training data (Lean proofs). But once the synthetic proofs are good enough, the system would self-train itself automatically.
https://leanprover.zulipchat.com/#streams/219941/Machine%20L...
The system I outlined above was inspired by this intriguing paper:
https://arxiv.org/abs/2207.14502
It is superficially about a different topic, namely generating and solving "programming puzzles", basically a type of unit test, that are then verified by the python interpreter. This system seems quite analogous to one where the programming puzzles are replaced by conjectures in a language like Lean, the proposed puzzle solutions are instead proposed proofs, and the python interpreter is replaced by the proof assistant.
I just discovered that there seems to be at least one guy working on applying a similar system to formal mathematics: https://www.cs.cmu.edu/~jlaurent/pdf/reports/thesis-proposal... He actually cites the paper above.
Regarding proving things about programs, no, it is not easy, and the developers do not seem to consider it a core goal of Lean.
I guess it depends on who you ask. The original devs of Lean wanted to do "everything" (because that's how you start projects, I guess). Since then it has attracted a lot of mathematicians (especially those working on Mathlib, a library that aspires to formalize "all known math") who are happy to have "algorithm objects" and prove things about them without being able to actually run an algorithm on any input.
This goes together with mostly embracing classical logic (which breaks the original and most powerful version of Curry-Howard, which allowed you to extract programs from proofs). However, in practical situations, algorithms extracted in this way tend to be too slow to be useful, so maybe that's not actually a downside for programming purposes.
Finally, Lean4 "compiles" to C-code, so at least it is (or can reasonably easily be made) portable. People have been trying to use it for real applications, like the AWS stuff others have linked in this thread.
You can see he is treating the case of k=1,2 with that formula and uses induction to extend it to 1 ≤ 𝑘 ≤ 𝑛 − 2.
For k = n - 1 he uses a different bound defined in equation 2.2. So he bypasses the issue.
Anyway, check out Idris[2], it’s cool for this sort of thing
I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).
By the way it is not clear to me, if the theorem was false or if only proof was wrong.
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!?
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.
“a strict superset of P” doesn’t really follow from that. P is also believed to be different from NP, and P is certainly not a strict superset of P.
Of course, I assume you just misspoke slightly, and that whatever it is that you actually meant to say, is correct.
E.g. maybe you meant to say “coNP is believed to both be strict superset of P (as is also believed about NP), and distinct from NP.”
I think it is believed that the intersection of NP and coNP is also a strict superset of P, but that this is believed with less confidence than that NP and coNP are distinct?
I imagine I’m not telling you anything you don’t already know, but for some reason I wrote the following parenthetical, and I’d rather leave it in this comment than delete it.
(If P=NP, then, as P=coP, then NP=P=coP=coNP , but this is considered unlikely.
It is also possible (in the sense of “no-one has yet found a way to prove otherwise” that coNP = NP without them being equal to P.
As a separate alternative, it is also possible (in the same sense) that they are distinct, but that their intersection is equal to P.
So, the possibilities: P=NP=coNP, P≠cocapNP=NP=coNP, P=cocapNP≠NP,coNP, All 4 are different, (cocapNP is the intersection of NP and coNP)
Where the last of these is I think considered most likely? )
The generalised quantum Stein's lemma [1][2] is (or was) a very powerful result that was used for over 10 years to prove things in this subfield. However last year it was noticed that there was an error in the proof of this lemma, and a whole bunch of results based on it weren't valid [3][4]. One of the authors of the paper where they wrote about the error gave a talk at the conference QIP 2023 this year, and there is a video of that talk available here [5]. Bartosz is a good speaker and I recommend watching the talk if you're interested, if you go to about 10 minutes, 30 seconds in the talk he discusses the consequences of this result now being not known to be true.
[1] Published paper https://link.springer.com/article/10.1007/s00220-010-1005-z
[2] Arvix version: https://arxiv.org/abs/0904.0281
[3] Published version: https://quantum-journal.org/papers/q-2023-09-07-1103/
[4] Arxiv version: https://arxiv.org/abs/2205.02813
[5] Youtube link: https://www.youtube.com/watch?app=desktop&v=2Xyodvh6DSY
Multiple papers on calculus claimed results about continuity and derivatives, but we’re using subtly different definitions.
The conflict between those results, and the counter-examples to demonstrate the difference, led to mathematicians building the modern machinery around proofs.
> The Weierstrass function has historically served the role of a pathological function, being the first published example (1872) specifically concocted to challenge the notion that every continuous function is differentiable except on a set of isolated points. Weierstrass's demonstration that continuity did not imply almost-everywhere differentiability upended mathematics, overturning several proofs that relied on geometric intuition and vague definitions of smoothness.
https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment.
Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.
Running a JavaScript codebase through the Typescript compiler is a lightweight way to do incremental proof checking, albeit it can only check proofs about the soundness of the code.
Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.
It just works surprisingly well for incrementally building up provable code properties.
For app dev I'd say the main problem is always "what we even need to build?", and then polishing over user experience.
One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.
>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.
> 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.
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.
However, from my experience as someone who scored "off the charts" on a UK school Cognitive Abilities Test and 148 on an IQ test: any score over 130 is suspect, as basically nobody is collecting enough data to make the tests statistically valid once you're more than 2σ from the mean.
Every source I've read or watched all agree the sample sizes used when creating the tests in the first place just aren't large enough to be all that confident beyond 2σ.
There's also the problem that training on tests is effective, which limits the ability of a test to be validated on those taking it fairly soon after it gets published.
A further other issue is that most IQ tests pre-suppose the existence of a G-factor and treat differences between types of intelligence as noise rather than a signal for the existence of any multi-factor variation. I don't know which hypothesis is correct (I lean towards thinking it's mostly a G-factor, but there are clearly some things which can only be explained by multi-factor models, e.g. where a skill is entirely absent such as in the case of dyscalculia).
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?
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?
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.
I'm sure for the prodigy-level students there is an even higher streamlined process for keeping them engaged.
https://youtu.be/Dp-mQ3HxgDE from 2019 at MS Research
https://www.youtube.com/watch?v=SEID4XYFN7o&t=4m35s (2022 at ICM international math congress)
Perhaps I should try sending him a mail
People approach things in a lot of different ways and it would be nice if we can just respect that instead of digging on each other or making unfounded assumptions.
I think your sentiment is misplaced as I would expect HN commenters to have heard of Tao as he often features in posts about mathematics. I'm sure I recall seeing some comments from him too.
There's an approachable Numberphile video featuring him here: https://www.numberphile.com/videos/the-worlds-best-mathemati...
https://x.com/8teapi/status/1713867160886599920?s=46&t=4jd61...
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...
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?