Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE)
The Project
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 Team
Andrej Bauer is the head of the Theoretical Computer Science Department at the Institute of Mathematics, Physics and Mechanics in Ljubljana, Slovenia, and a professor of computational mathematics at the University of Ljubljana. Bauer’s work spans foundations of mathematics, constructive and computable mathematics, type theory, homotopy type theory, formalized mathematics, and mathematical principles of programming languages. He is also known for his seminal work on programming with algebraic effects and handlers.
Primož Potočnik is the leader of the research group on computationally intensive methods in mathematics at the Institute of Mathematics, Physics and Mechanics in Ljubljana, and a professor of mathematics at the University of Ljubljana, Slovenia. His work focuses on symmetry in combinatorial and algebraic structures. He is recognized in the mathematical community for his datasets of highly symmetrical graphs and maps.
Ljupčo Todorovski is a professor of computer science at the Faculty of Mathematics and Physics at the University of Ljubljana. His research interests lie in artificial intelligence, with a particular focus on developing machine learning algorithms for computational discovery of scientific knowledge and models from experimental data. Recently, he has been collaborating with mathematicians to design AI tools that support formalization of mathematics with proof assistants.
Danel Ahman is an Associate Professor of Programming Languages at the Institute of Computer Science, University of Tartu, Estonia. His research focuses on programming language theory, particularly the design and meta-theory of programming languages with advanced type systems. He works on using types to formally specify and verify how and when programs use data and resources, on developing compositional type-theoretic models for data structures, and on applying these techniques to build correct-by-construction, verified software.
Katja Berčič is a researcher at the Institute of Mathematics, Physics and Mechanics and a teaching assistant at the University of Ljubljana, Slovenia. She works on the development of robust and interoperable infrastructure for mathematical data and its integration with mathematical software. Her work is grounded in an analysis of how mathematicians create, structure, and interact with data in practice. She also investigates how these activities relate to the broader context of research data management.