How Terry Tao Became an Evangelist for AI in Math | Quanta Magazine

With automated proof-checkers, a problem can be broken up into small chunks, solved bit-by-bit, then reassembled with confidence that every piece is correct. For some, this heralds a new area in mathematical research.

https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

#TopNews #News #Tao #Lean #EquationalTheories

A very nice article in @QuantaMagazine mentions our #EquationalTheories project, led by @tao, which aims to advance collaborative mathematical research at scale through the synergy of human researchers, interactive proof assistants (@leanprover) and automated theorem provers.

https://www.quantamagazine.org/mathematical-beauty-truth-and-proof-in-the-age-of-ai-20250430