BRIDGE
The BRIDGE project aims to integrate AI with proof assistants and mathematical data by creating and curating large-scale datasets and dependency graphs from formalized mathematics libraries. The team will develop AI-based tools to support the formalization and exploration of mathematical structures, proofs, and their interdependencies. These tools, including a recommendation system and user-guided discovery features, are expected to improve both accessibility and efficiency in mathematical reasoning.
The project is funded by Renaissance Philanthropy through its AI for Math Fund.
MathQL
MathQL is a typed query language for asking questions about databases of mathematical objects.
Mathswitch
Mathswitch is a prototype that gathers mathematical concepts from around the web into one place.
Bridge MCP
Bridge MCP is a server that lets AI agents ask questions about mathematical objects.
Symmetric Objects
We link existing datasets of highly symmetric structures and prepare them for proof assistants.