Advancing mathematics research with generative AI

TL;DR

Generative AI models, despite not being primarily logical, can assist mathematicians by recognizing complex patterns, generating proofs, and integrating with formal systems to accelerate mathematical research.

Contribution

This paper explores how generative AI can be leveraged as an interactive tool to enhance advanced mathematics research, including integration with formal proof systems.

Findings

AI models can identify patterns in higher mathematics

Generative AI can assist in proof generation and debugging

Integration with formal systems enhances mathematical research

Abstract

The main drawback of using generative AI models for advanced mathematics is that these models are not primarily logical reasoning engines. However, Large Language Models, and their refinements, can pick up on patterns in higher mathematics that are difficult for humans to see. By putting the design of generative AI models to their advantage, mathematicians may use them as powerful interactive assistants that can carry out laborious tasks, generate and debug code, check examples, formulate conjectures and more. We discuss how generative AI models can be used to advance mathematics research. We also discuss their integration with neuro-symbolic solvers, Computer Algebra Systems and formal proof assistants such as Lean.