⊕ Dataset · mathlib-rdf · 2026-04
MathLib RDF · Knowledge Graph
Knowledge graph over Mathlib statements, materialised from the SciLib ontology. Typed edges usesInType / usesInValue, domain taxonomy with provenance. The first step toward a semantic description of scientific knowledge beyond mathematics.
MathLib RDF is the materialisation of the SciLib ontology over the largest formalized library of mathematics (Mathlib, Lean4). Concrete TBox content over the corpus: 213 000+ statements as entities, typed dependency edges, a domain taxonomy of 660+ subclasses with source provenance.
What's in the graph
- Nodes: Mathlib statements (theorems, definitions, instances), SciLib ontology classes (TBox), Lean types.
- Edges:
usesInType,usesInValue,derivedFrom,interpretedRelation(TBox-driven). - Metadata: module, docstring, Lean attributes, library version.
Why
The graph already powers Graph RAG (Lean4 premise retrieval), MathLib Explorer (graph navigation for researchers), premise-retrieval benchmarks. Next — extending beyond mathematics: theoretical physics, formal logic, information theory; linking formalized results to preprints and journal publications through ORCID/DOI.
Access
SPARQL endpoint on GraphDB (internal); MCP tool sparql_query (POST /mcp/tools/call) is public. Full dump on request.