Anima Anandkumar and Sergei Gukov Receive AI+Math DARPA Grant
Anima Anandkumar, Bren Professor of Computing and Mathematical Sciences, and Sergei G. Gukov, John D. MacArthur Professor of Theoretical Physics and Mathematics, have been working together on the unsolved mathematical problem in group theory known as the Andrew-Curtis or AC conjecture. They formalized the AC conjecture in Lean, and leveraged LLMs for theorem discovery.
Professor Anandkumar's group has a track record of frontier research in AI+Math. They introduced Leandojo in 2023, the first open-source framework for hallucination-free mathematical reasoning that combined large language models (LLM) with Lean, a formal prover. They also introduced LeanAgent a year later, a lifelong learning LLM agent that continues to expand on its mathematical knowledge in Lean. Recently, their TorchLean extends formal verification to neural network systems such neural control systems and physics-informed neural networks where verification of neural systems is needed. "By combining frontier AI reasoning systems with deep mathematical understanding from our two groups, we are excited to push the boundaries of what is possible" says Anima Anandkumar.
