Advancing mathematics research with generative AI
This work offers a solution for mathematicians by integrating generative AI with tools like Computer Algebra Systems and formal proof assistants, though it is incremental as it builds on existing AI capabilities.
The paper addresses the limitation of generative AI models in logical reasoning for advanced mathematics, proposing their use as interactive assistants to perform tasks like code generation, debugging, and conjecture formulation, thereby advancing mathematics research.
The main drawback of using generative AI models for advanced mathematics is that these models are not 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 Computer Algebra Systems and formal proof assistants such as Lean.