Search papers, labs, and topics across Lattice.
This paper introduces Matlas, a semantic search engine designed to enhance the retrieval of mathematical knowledge from a vast corpus of over 8 million statements derived from 435,000 peer-reviewed papers and textbooks. By constructing document-level dependency graphs and recursively unfolding statements, Matlas provides self-contained representations that improve the interpretability of mathematical results. The system enables efficient natural language search, significantly aiding mathematicians and AI systems in accessing relevant theorems and historical contexts.
Matlas transforms mathematical literature retrieval by enabling intuitive natural language searches across a vast database of interconnected mathematical statements.
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.
