AI for Math fund

Renaissance Philanthropy and XTX Markets have announced the launch of the AI for Math Fund, a new grant program supporting projects that apply AI and machine learning to mathematics, with a focus on automated theorem proving, with an initial $9.2 million in funding. The project funding categories, and examples of projects in such categories, are:

1. Production Grade Software Tools

• AI-based autoformalization tools for translating natural-language mathematics into the formalisms of proof assistants
• AI-based auto-informalization tools for translating proof-assistant proofs into interpretable natural-language mathematics
• AI-based models for suggesting tactics/steps or relevant concepts to the user of a proof assistant, or for generating entire proofs
• Infrastructure to connect proof assistants with computer algebra systems, calculus, and PDEs
• A large-scale, AI-enhanced distributed collaboration platform for mathematicians

2. Datasets

• Datasets of formalized theorems and proofs in a proof assistant
• Datasets that would advance AI for theorem proving as applied to program verification and secure code generation
• Datasets of (natural-language) mathematical problems, theorems, proofs, exposition, etc.
• Benchmarks and training environments associated with datasets and model tasks (autoformalization, premise selection, tactic or proof generation, etc.)

3. Field Building

• Textbooks
• Courses
• Documentation and support for proof assistants, and interfaces/APIs to integrate with AI tools

4. Breakthrough Ideas

• Expected difficulty estimation (of sub-problems of a proof)
• Novel mathematical implications of proofs formalized type-theoretically
• Formalization of proof complexity in proof assistants

The deadline for initial expressions of interest is Jan 10, 2025.

[Disclosure: I have agreed to serve on the advisory board for this fund.]