Formal verification – also known as “automated theorem proving” – allows computers to rigorously verify the correctness of proofs, or more broadly to “prove” the correctness of computer programs. Unfortunately, these tools are quite technically involved and their development is under-resourced, limiting their adoption primarily to formal verification researchers. With the advent of AI technologies such as large language models (LLMs), the barrier to entry for these formal tools is dropping rapidly, and making formal verification frameworks accessible to working mathematicians. Advances in AI reasoning also have massive potential to expedite and support proof search efforts. As a result, AI can be a transformative force that can catalyze mathematical research, drive further collaboration across the field, and scale formalization and theorem proving to previously impossible levels, leading to faster advancements in mathematics and science.

AI for math has seen a growing number of exciting results from industry labs and academic researchers alike. However, open-source projects that benefit the field as a whole are underfunded both by industry and by traditional academic grants. Although the National Science Foundation has a modest program at the intersection of AI and math ($6 million per year), increased support can advance both the pace and impact of math discovery.