Matlas: A Semantic Search Engine for Mathematics

• URL: http://arxiv.org/abs/2604.17484v1
• Date: Sun, 19 Apr 2026 15:17:28 GMT
• Title: Matlas: A Semantic Search Engine for Mathematics
• Abstract summary: Matlas is a semantic search engine for mathematical statements.<n>Matlas is built on a large-scale corpus of 8.07 million statements extracted from 435K peer-reviewed papers spanning 1826 to 2025.<n>On top of this corpus, we develop a semantic retrieval system that enables efficient search for mathematical results using natural language queries.
• Score: 2.8548596155460024
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• The zbMATH Open Knowledge Graph: Tracing Centuries of Mathematical Research [2.2549386819889734]
  The zbMATH Open KG is a large-scale RDF knowledge graph covering more than 250 years of mathematical scholarship.<n>The graph comprises 34 million entities and 168 million RDF triples represented using established Semantic Web vocabularies.
  arXiv  Detail & Related papers  (2026-09-01T09:27:06Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• MathAtlas: A Benchmark for Autoformalization in the Wild [7.981378950583468]
  We introduce MathAtlas, the first large-scale autoformalization benchmark of in the wild graduate-level mathematics.<n>MathAtlas contains 52k theorems, definitions, exercises, examples, and extracted from 103 graduate mathematics textbooks.
  arXiv  Detail & Related papers  (2026-05-13T19:35:46Z)
• HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification [54.06301039725887]
  We introduce HorizonMath, a benchmark of over 100 predominantly unsolved problems spanning 8 domains in computational and applied mathematics.<n>Our benchmark targets a class of problems where discovery is hard, requiring meaningful mathematical insight, but verification is computationally efficient and simple.
  arXiv  Detail & Related papers  (2026-03-16T17:59:53Z)
• Semantic Search over 9 Million Mathematical Theorems [0.31229177276953496]
  We introduce and study semantic theorem retrieval at scale over a unified corpus of $9.2$ million theorem statements extracted from arXiv and seven other sources.<n>We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality.
  arXiv  Detail & Related papers  (2026-02-05T02:16:20Z)
• AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database [1.799933345199395]
  A mathematical knowledge graph (KG) presents knowledge within the field of mathematics in a structured manner.<n>This paper proposes AutoMathKG, a high-quality, wide-coverage, and multi-dimensional math KG capable of automatic updates.
  arXiv  Detail & Related papers  (2025-05-19T17:41:29Z)
• Mathematical Entities: Corpora and Benchmarks [0.8766411351797883]
  There has been relatively little research on natural language processing for mathematical texts. We provide annotated corpora that can be used to study the language of mathematics in different contexts.
  arXiv  Detail & Related papers  (2024-06-17T14:11:00Z)
• OntoMath${}^{\mathbf{PRO}}$ 2.0 Ontology: Updates of the Formal Model [68.8204255655161]
  The main attention is paid to the development of a formal model for the representation of mathematical statements in the Open Linked Data cloud. The proposed model is intended for applications that extract mathematical facts from natural language mathematical texts and represent these facts as Linked Open Data. The model is used in development of a new version of the OntoMath$mathrmPRO$ ontology of professional mathematics is described.
  arXiv  Detail & Related papers  (2023-03-17T20:29:17Z)
• How Do Transformers Learn Topic Structure: Towards a Mechanistic Understanding [56.222097640468306]
  We provide mechanistic understanding of how transformers learn "semantic structure" We show, through a combination of mathematical analysis and experiments on Wikipedia data, that the embedding layer and the self-attention layer encode the topical structure.
  arXiv  Detail & Related papers  (2023-03-07T21:42:17Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  We review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade. Recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning.
  arXiv  Detail & Related papers  (2022-12-20T18:46:16Z)
• Self-Supervised Pretraining of Graph Neural Network for the Retrieval of Related Mathematical Expressions in Scientific Articles [8.942112181408156]
  We propose a new approach for retrieval of mathematical expressions based on machine learning. We design an unsupervised representation learning task that combines embedding learning with self-supervised learning. We collect a huge dataset with over 29 million mathematical expressions from over 900,000 publications published on arXiv.org.
  arXiv  Detail & Related papers  (2022-08-22T12:11:30Z)
• Learning to Match Mathematical Statements with Proofs [37.38969121408295]
  The task is designed to improve the processing of research-level mathematical texts. We release a dataset for the task, consisting of over 180k statement-proof pairs. We show that considering the assignment problem globally and using weighted bipartite matching algorithms helps a lot in tackling the task.
  arXiv  Detail & Related papers  (2021-02-03T15:38:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.