How AI Could Be A Mathematician's Co-Pilot by 2026 (Prof. Swarat Chaudhuri)

COPRA Framework

The COPRA framework, a GPT-based tool for formal theorem proving, represents a significant advancement in AI's role in mathematics. Swarat Chaudhuri explains that COPRA utilizes a large language model to predict tactics for theorem proving without fine-tuning, a departure from previous methods that relied on models trained on proof data 1. This approach allows COPRA to effectively use external knowledge bases and perform in-context learning, even in complex mathematical settings 2.

The main finding in that paper is that in-context learning can be interesting even in this setting.

--- Swarat Chaudhuri

The framework's ability to backtrack and learn from failed attempts enhances its problem-solving capabilities, showcasing the potential of AI in formal theorem proving 2.

   

Symbolic Regression

Symbolic regression, a form of neurosymbolic programming, leverages AI to simplify and solve mathematical expressions. Swarat Chaudhuri describes symbolic regression as a type of program synthesis where AI finds expressions that fit datasets, using methods like neural admissible heuristics 3. This process can be enhanced by employing large language models (LLMs) to guide the search and abstraction of programs, allowing for creative exploration within grounded data constraints 4.

You could imagine a loop where you come up with candidates creatively using an LLM, you empirically evaluate these candidates and then you use the experience to basically fine tune the model further.

--- Swarat Chaudhuri

This iterative approach not only builds on prior knowledge but also enables the development of new scientific insights, demonstrating the transformative potential of AI in mathematical discovery 4.