#math #plebchain
I really like Terence Tao. Especially during this LLM hyper, his attitude has been very objective and neutral - not overhyping or dismissing it, but just quietly doing various experiments. So I trust his judgment a lot.
I watched this video from his presentation at international math olympiad competition about AI and mathematics, and a few points that impress me a lot:
GPT-4 claiming to solve IMO problems is a cherry-picked example: First, what was fed to GPT wasn't the original problem, but a simplified version (to make it easier for GPT to understand). Second, out of several hundred IMO-level problems tested, the success rate was only about 1%. In other words, GPT doesn't yet have the ability to solve IMO-level math problems.
In 1976, the Four Color Theorem was the first major theorem proved with computer assistance. In 1996, a truly computer-verifiable proof was made. In 2005, a fully formalized proof was made using the Coq proof assistant.
AI will become very good at generating good conjectures, expanding mathematical research to an unprecedented scale.
This is a bit off-topic, but I noticed that Terence Tao is more of a research type and not particularly skilled at public speaking. He spent the whole time either looking at slides or the floor, speaking directly and plainly, without vocal inflections or performative elements. I actually find it quite cute, haha!
(ps: i post this from coracle again, after a while! it feels good!)
