⊕ Датасет · mathlib-rdf · 2026-04
MathLib RDF · Knowledge Graph
Граф знаний над утверждениями Mathlib, материализованный из онтологии SciLib. Типизированные рёбра usesInType / usesInValue, доменная таксономия с провенансом. Первый шаг к семантическому описанию научного знания за пределами математики.
MathLib RDF — материализация онтологии SciLib над крупнейшей формализованной библиотекой математики (Mathlib, Lean4). Конкретное предметное наполнение TBox-онтологии: 213 000+ утверждений как сущности, типизированные рёбра зависимостей, доменная таксономия из 660+ подклассов с провенансом источника (модуль Mathlib, версия библиотеки, докстринг).
Что в графе
- Узлы: утверждения Mathlib (теоремы, определения, инстансы), классы онтологии SciLib (TBox), типы Lean.
- Рёбра:
usesInType(используется в типе сигнатуры),usesInValue(используется в теле),derivedFrom,interpretedRelation(связи по TBox). - Метаданные: модуль, докстринг, атрибуты Lean (simp, decidable, type-class), версия библиотеки.
Зачем
На графе работает Graph RAG (подбор лемм для Lean4), MathLib Explorer (графовая навигация для исследователя), бенчмарки подбора посылок. В перспективе — расширение за пределы математики: теоретическая физика, формальная логика, теория информации; связывание формализованных результатов с препринтами и журнальными публикациями через ORCID/DOI.
Доступ
SPARQL-эндпоинт GraphDB — внутренний; MCP-tool sparql_query (POST /mcp/tools/call) — публичный. Полный дамп — по запросу.