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.

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!

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.

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?

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.

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.