SciLib
Лаборатория семантического анализа научных данных. Онтология, граф знаний и векторное пространство — единый контракт.
Активные проекты
Что мы делаем
Семантический контракт между формальной онтологией, графом знаний и векторным пространством. Первая предметная область — математика: Lean4 Mathlib.
MathLib Explorer
Семантический и графовый поиск по 213 000+ утверждениям Mathlib. Навигация по типизированным зависимостям между теоремами.
Открыть → ⊢Graph RAG
Подбор лемм для целей Lean4 поверх формального графа знаний. Восемь шагов pipeline, без обращений к LLM на горячем пути.
Открыть → ∂Лаборатория
Опубликованные исследования, открытые модели и датасеты лаборатории SciLib.
Открыть →Журнал
Из блога
FAIR - как сделать данные полезными
FAIR-принципы - это набор рекомендаций, который обеспечивает для данных и знаний, чтобы они были легко находимыми, доступными, совместимыми между системами и пригодными для многократного использования людьми и машинами.
20 Июн 2026 · O. Ataeva ∇Что такое W3C PROV
W3C PROV — это международный стандарт, который позволяет описывать происхождение данных и прослеживать, какие объекты, процессы и участники привели к появлению того или иного результата, обеспечивая прозрачность, воспроизводимость и доверие к информации и системам искусственного интеллекта.
20 Июн 2026 · O. Ataeva ∇Simplex over pairs: geometry of multimodal mathematics
Why SciLibModal uses centroid geometry instead of the pairwise CLIP scheme.
04 Май 2026 · A. KhalovО проекте
SciLib — лаборатория семантического анализа научных данных. Мы строим инфраструктуру, в которой смысл научного объекта (что он значит), форма (как он выражен — текст, формула, код, изображение) и носитель (где и как он хранится) разделены и связаны явными семантическими отношениями. Эта архитектура обеспечивает инвариантность к адресату: одно и то же знание читается человеком и обрабатывается программой без потери семантики.
Первая предметная область — формализованная математика. На её материале выстроены: онтология SciLib (модульная OWL/DL, три уровня описания), граф знаний над Mathlib (213 000+ утверждений, типизированные рёбра usesInType/usesInValue, 660+ доменных подклассов), мультимодальная векторизация и подбор лемм через детерминированное расширение по графу.
Все компоненты доступны через публичные API: /grag/* — подбор лемм и верификация Lean4, /mcp/* — семантический поиск, графовые запросы, доступ к корпусу. Большинство артефактов распространяется по открытым лицензиям с указанием авторов.