Everyone should read the celebrated mathematician Terence Tao's blog on LLM. He predicts that AI will be a trustworthy co-author in mathematical research by 2026, when combined with search and symbolic math tools. I believe math will be the first scientific discipline to see major breakthroughs enabled by AI, because math: ▸ can be expressed conveniently as a coding problem. Strings are naturally first-class citizens. ▸ can be rigorously verified by theorem provers like Lean, rather than relying on empirical results. ▸ does not require physical experiments like biology & medicine. Robotics isn't ready yet. We are already seeing big progress: ▸ LeanDojo (leandojo.org/) from my colleagues @NVIDIAAI & @Caltech is among the first steps towards this grand challenge. ▸ Last year, OpenAI used Lean to solve some math olympiad problems: openai.com/research/formal-m… ▸ ChemCrow is another example, but for chemistry. It integrates GPT-4 with professional tools like molecular synthesis planner and reaction prediction: arxiv.org/abs/2304.05376 ▸ Terrance Tao's blog: unlocked.microsoft.com/ai-an…