∇ Catalogue

Models

Open models and services of the SciLib lab: the multimodal encoder SciLibModal, the formal SciLib Ontology, the production Graph RAG Endpoint. Most artifacts are under open licenses with attribution; some are available on request.

grag C21

Graph RAG Endpoint

Production service for Mathlib premise retrieval and Lean4 verification. GraphDB + PostgreSQL + Qdrant + Lean REPL. Endpoints /grag/search and /grag/check, no LLM calls on the hot path.

REST API · 8 steps · 0 LLM on the hot path API — public; responses — CC BY-NC 4.0

scilib-onto v1.0

SciLib Ontology

Modular ontology of scientific knowledge. Strictly separates three levels of object description: interpretation (what it means), representation (how it is expressed), resource (where it is stored). Domain instantiation — mathematics (660+ subclasses), materialised over Mathlib.

660+ domain subclasses · modular OWL/DL CC BY 4.0

slm-modal v2

SciLibModal

Multimodal encoder: a scientific object is modelled as a simplex in a shared 312-dim space. Vertices are modalities (EN, RU, Lean4, LaTeX, image); the centroid is an aggregate representation invariant to the choice of modality.

312-dim · 5 modalities · simplex geometry API — public; weights — on request with attribution