∇ Исследования
MathLib RDF: первый шаг к семантической карте науки
Зачем мы строим RDF-граф над Mathlib и почему это начало большого проекта.
Mathlib — крупнейшая в мире формализованная библиотека математики: 213 000 утверждений, прошедших проверку Lean4, в одной согласованной системе типов. Для исследователя это огромное богатство; для машинного поиска — пока что плоский каталог имён, который не виден целиком. Мы строим над Mathlib семантический слой — граф знаний MathLib RDF.
Что значит «семантический»
В RDF-графе каждое утверждение представлено как узел с типизированными связями: какие определения оно использует в типе сигнатуры, какие — в теле доказательства, какие тактики применялись, к какому модулю Mathlib относится. Эти связи — формальные: не «похоже на», а «извлечено из самого Lean-кода и проверено компилятором». Поверх корпуса проложена онтология SciLib v1.0.0 — 670+ классов в логике ALCHIQ(D), описывающий категории математических объектов и стандартные предикаты связи.
Зачем
На этом графе уже работает Graph RAG: подбор лемм через расширение по графовым связям, без галлюцинаций. Работает MathLib Explorer: графовая навигация для исследователя. Работают бенчмарки подбора лемм: цифры, которые легко воспроизвести. Это — текущий день.
Большой проект
MathLib RDF — первый шаг. Дальше — расширение онтологии на смежные области: теоретическая физика, теория информации, формальная логика. Связывание формализованных результатов с препринтами и журнальными публикациями: для каждого утверждения Mathlib — какая статья его впервые доказала, в каком виде, в каком журнале. Интеграция с реестрами авторов (ORCID) и идентификаторами публикаций (DOI). Семантический поиск по научной литературе с привязкой к формальному ядру.
Долгосрочная цель — единый граф научного знания, в котором каждое утверждение имеет адресуемый идентификатор, связан с публикациями и авторами, и проверяем (где это возможно) формальной верификацией. Не всё научное знание поддаётся формализации сегодня — но математика и теоретическая физика поддаются, и это естественные первые слои.
Если ваша исследовательская группа работает с формализацией в Lean4 / Coq / Isabelle / Agda / Metamath, или с цифровыми библиотеками научной литературы — давайте обсудим интеграцию: info@scilibai.ru.