Big Math Libraries in Interactive Theorem Provers

Explore the concept of Big Math and its implementation in Interactive Theorem Provers (ITPs) with Fabian Huch from the Hausdorff Center for Mathematics. Delve into the five central aspects of Big Math: inference, computation, concretization, narration, and organization. Examine the challenges and solutions related to library sizes, searching capabilities, integration processes, build schedules, guidance tooling, and maintenance in the context of large mathematical libraries. Gain insights into the complexities and strategies involved in managing and utilizing extensive mathematical knowledge within ITPs during this informative 35-minute talk.