Katja Berčič: Databases of mathematical structures for formalization and AI

Abstract: In the BRIDGE project, mathematical data play a central role alongside AI and formalization. I will begin with a brief overview of the key mathematical datasets and databases relevant to BRIDGE, emphasizing their data formats, interoperability challenges, and prospects for integration. A central component of this effort is MathDataHub, a platform for hosting collections of examples of mathematical structures; I will outline its architecture and the features that enable interaction with proof assistants. I will then discuss insights from Lean-HoG, our prototype integration of Lean with the House of Graphs, and explain how these lessons inform planned extensions of MathDataHub within BRIDGE to support smoother integrations. Finally, I will outline our plan to organize several related datasets and make them available for both AI applications and formalization efforts.