Graph RAG Endpoint · SciLib

∇ Model · 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

Graph RAG Endpoint is the lab's production service. It implements the SciLib-GRC21 pipeline as a REST API.

Endpoints

  • POST /grag/search — Lean4 goal → categorised lemma hints (apply / rw / simp / def). 0 LLM calls on the hot path; typical latency < 200 ms.
  • POST /grag/check — Lean4 proof verification via REPL (Mathlib v4.28.0-rc1 preloaded).
  • GET /grag/info — pipeline / version description.
  • GET /grag/health — health check.

How to use

No registration, no API keys. Industrial integrations — via info@scilibai.ru. Demo at Graph RAG.

Tags: api, graph-rag, premise-selection, lean4, mathlib

← To the catalogue