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