Skip to content(if available)orjump to list(if available)

Terence Tao – Machine-Assisted Proofs [video]

Terence Tao – Machine-Assisted Proofs [video]

6 comments

·February 22, 2025
Visit

ipnon

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.

yo_yo_yo-yo

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”.

ipnon

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.

newswasboring

> 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.

isolli

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...