Matlas: A Semantic Search Engine for Mathematics

TL;DR

Matlas is a large-scale semantic search engine for mathematical statements, enabling efficient retrieval of mathematical results from a vast corpus using natural language queries, supporting mathematicians and AI systems.

Contribution

The paper introduces Matlas, a novel semantic search engine built on a large, dependency-structured corpus of mathematical statements from diverse sources.

Findings

Built a corpus of 8.07 million statements from 435K papers and textbooks.

Constructed dependency graphs and unfolded statements for self-contained representations.

Developed a semantic retrieval system for natural language search of mathematical results.

Abstract

Retrieving mathematical knowledge is a central task in both human-driven research, such as determining whether a result already exists, finding related results, and identifying historical origins, and in emerging AI systems for mathematics, where reliable grounding is essential. However, the scale and structure of the mathematical literature pose significant challenges: results are distributed across millions of documents, and individual statements are often difficult to interpret in isolation due to their dependence on prior definitions and theorems. In this paper, we introduce Matlas, a semantic search engine for mathematical statements. Matlas is built on a large-scale corpus of 8.07 million statements extracted from 435K peer-reviewed papers spanning 1826 to 2025, drawn from a curated set of 180 journals selected using an ICM citation-based criterion, together with 1.9K textbooks. From these sources, we extract mathematical statements together with their dependencies, construct document-level dependency graphs, and recursively unfold statements in topological order to produce more self-contained representations. On top of this corpus, we develop a semantic retrieval system that enables efficient search for mathematical results using natural language queries. We hope that Matlas can improve the efficiency of theorem retrieval for mathematicians and provide a structured source of grounding for AI systems tackling research-level mathematical problems, and serve as part of the infrastructure for mathematical knowledge retrieval.