Terence Tao – Machine-Assisted Proofs [video] | Hacker News Reader

Terence Tao – Machine-Assisted Proofs [video]

youtube.com

111 pointsipnon31 comments

One thing he does point out closer to the conclusion is that currently they haven't found LLMs to be particularly useful, and notes also that AlphaProof is currently not quite there yet in writing succinct proofs. Nonetheless, he seems to be optimistic and thinks that these models will improve quickly.

I wanted to use this moment to be simply impressed by how much 'intelligence' we can get out of many people working towards a common goal with the same ideals. The most recent and biggest advances and progress in machine-assisted proofs has been, according to Tao, the improvements in more traditional communication/organisation/automatisation processes. This enabled many humans to put their efforts together and establish the foundations for future mathematics. So incredible.

As an ex-mathematician I was really interested to see how well o3 etc handles difficult, unseen math questions, so I tried giving it some hard-ish questions from mathoverflow [1] (mainly non-trivial questions on graduate+ level topics). It definitely isn't great and may even be more harmful than useful currently. The main issue it will never say "I'm not sure how to do this", it will almost always give a complete answer from start to finish, with 'bugs' along the way that can be very subtle.

But I found it genuinely shocking some of the steps it manages to take successfully, and it definitely doesn't feel like we're a million years from something could replace big parts of researchers' work. I honestly found some things it could do extremely unsettling as a thought-worker.

[1] https://mathoverflow.net/

not sure _how_ relevant it is at the bottom line but you are aware that o3 was trained very likely on those same problems form mathoverflow? cause you know - the underlying llm was trained on pretty much everything available oline - especially high quality sources like ... mathoverflow.

I was posting questions from the last week, so not in o3 training data.

I saw this talk in person, and I liked so much it inspired to spend four years doing a PhD in automated theorem proving.

As things stand, I'm starting one this October!

Congrats, and good luck!

Thanks!

If anybody has any suggestion in preparing for a PhD in a major university, I'd appreciate it: I expect these four years to be fun but also very challenging.

I completed my PhD in neuroscience at a mid-tier university.

One piece of advice I can give you is to stay focused, but keep sight of the freedom and flexibility your time as a grad student will offer you.

I was lucky to have an advisor that granted me flexibility to learn topics outside of his expertise through self-study and collaborations. That flexibility ended up shaping my early career.

The last quip I’ll give you is to prioritize your physical and mental health. Go to the gym/run/exercise, meditate, and eat enough. Grad school is difficult, and peripheral health issues make it worse.

Your work is nothing if you don't become part of the community. As much as the lone genius meme can be appealing when you're a PhD student, academia is the realm of anonymous reviews, grant-based survival and kafkaesque bureaucracy. If you don't fit into a research community which will give you support, that's all you'll be left with. That and a stack of worthless papers.

I wasn’t aware that mathematicians are able to collaborate en masse on proofs now with Lean just like software engineers can make 10 pull requests to the same file in a day.

That’s the main thing that Tao identifies that Lean enables, collaboration where Lean does the work of checking the output of the collaborator, thus becoming a force multiplier. There’s still the issue of how the proof should be organized, how it should be factored into various implications, and here, like in the Linux kernel, contributors with seniority referee the process, as Tao did with his “experiment”.

Now imagine using Devin on the boring bits! “I remember seeing this proved before but I can’t be bothered to go look it up again.” It’s easy to imagine an explosion of interesting results soon.

> I remember seeing this proved before but I can’t be bothered to go look it up again.

I think that is what Lean libraries are for.

Possibly but lean libraries currently contain a tiny fraction of widely known mathematical results.

I remember, as a child, reading and wondering about the computer-assisted proof of the four color theorem. (The first major theorem to be proven so, according to Wikipedia.)

https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_co...

What’s different about Lean compared to older theorem provers like Coq and Isabelle? I mean mathematicians could’ve used Coq / Isabelle / etc for decades for the same purpose. Why didn’t they? What’s does Lean do differently that excites mathematicians and makes it more appealing?

I think two primary things, which are connected. First, Kevin Buzzard, a “real” mathematician (as he self-identifies), promoted computer formalization of research mathematics with the Xena project, and second when looking for tools he latched onto Lean because he felt it more ergonomic. [1]

He later discovered why Coq, Isabelle/HOL, and other tools did things in certain ways [2] (which were more “natural” to computer scientists) but by then his advocacy and inertia (the growing, curated MathLib) cemented Lean as the tool mathematicians tried first and sort of stuck with.

[1] https://news.ycombinator.com/item?id=21200721

[2] https://xenaproject.wordpress.com/2020/07/03/equality-specif...

Opinion, but lean and coq both use dependant type theory, while isabelle uses a first order logic. Between coq and lean, lean has always had great support for unicode, where coq always seemed to me ascii first, and coq itself predates the publishing of the unicode standard and formation of the unicode consortium. At least my feeling has always been that syntax probably takes no small part in it. Because with lean one can use all the familiar mathematical alphanumeric symbols and operators.

Isabelle is a generic theorem prover. It supports the standard set theory on first order logic as well, but it's most popular logic is HOL, which is a kind of type theory. Isabelle is well integrated with LaTeX, so its support for mathematical symbols goes beyond unicode. One can write complete well typeset mathematical papers inside Isabelle, and people do. So it's not that. Yet, the dynamics of Lean uptake among mathematicians is much better, so I am curious why is that. I would really like to see an opinion of someone who knows both Lean and Isabelle well, but prefers Lean for formalized mathematics. Or is that all coincidence and hype?

I am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize.

This experiment did use 'lean', but it is very important to have real-life altertnative formal solver at a low technical cost.

This makes me wonder if math will ever reach a point where it’s “solved”. Like, a point where we know everything there is to know and every new field that you can think of can already be mapped to something else.

Gödel says no

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

Naturally, by “everything there is to know” I meant within the confines of what’s possible to know

You should read godel escher bach by hofstadter.

Then I'm curious: is it possible to know when we know everything there is to know?

Good question. I don’t know!

The answer is no. There are statements for which knowing if they are decidable is undecidable.

I know that \exists undecidable statements, I just don't know if this specific statement is decidable...

Note that being able to do this would imply P=NP.

I could listen to Terence speak all day. To be that smart and be able to communicating effectively to a noob like me is a rare skill.

Reply on news.ycombinator.com