Oblast AI, kde počítače dokazují matematická tvrzení. Moderní systémy kombinují formální nástroje typu Lean s jazykovými modely a výzkumnými agenty, kteří zkoušejí různé postupy a sdílejí dílčí výsledky i neúspěšné přístupy, aby neopakovali práci ostatních. Cílem je urychlit matematický výzkum — počítač pomáhá dokázat věty, na které by lidé potřebovali měsíce nebo roky.
