MATRIX-MFO Tandem Workshop: Machine Learning and AI for Mathematics

Abstract

This workshop explored how modern machine learning can both accelerate mathematical discovery and preserve rigorous standards. It focused on three angles: using AI techniques to help mathematicians make advances on challenging problems; using mathematics to understand AI predictions; and using deep-learning models for automated theorem proving. Key discussions included using machine learning as a tool for constructing interesting mathematical constructions and navigating in mathematical search spaces, to uncover conjectures and high-quality examples (e.g., sphere packings via DiffuseBoost, combinatorial objects via AlphaEvolve); Integrating Large Language Models (LLMs) with formal systems (e.g., Lean/mathlib) to create scalable, certifiable AI-based automated theorem prover; Collaborative formalization (e.g., the Carleson theorem project), autoformalization for high-quality supervised data, and reinforcement learning/search methods for proof generation and algorithmic reasoning.