---
license: apache-2.0
library_name: pytorch
tags: [lean-4, mathlib, theorem-proving, gnn, tactic-prediction, premise-retrieval]
language: [en]
---

# Mathlib joint-source GNN + GRU

Complete pre-template research system: normalized graph encoder, tactic head,
GRU argument decoder, explicit argument-count head, per-position local/library
source gate, local selector and contextual library scoring. Maximum three flat
arguments. Weights include joint stage epoch 3, local-only refinement
epoch 8, and matched dual-encoder/index epoch 5.

## Loading

```python
from huggingface_hub import snapshot_download
from maths_ai.gnn_inference.atp_lean_gnn.joint_bundle import load_joint_source_bundle
path = snapshot_download("iCogLabs-Dev/Mathlib-Sexpr-GNN", revision="<release-tag-or-commit>")
system = load_joint_source_bundle(path, device="cpu")
```

`system.policy`, `system.retriever`, `system.lemma_index`, and vocabularies are
available separately. `retrieve(original_state_texts)` performs live text
retrieval. `predict(batch, original_state_texts, graph_format="lean-model-sexp-v2")`
expects correctly normalized prepared PyG graphs and their original state text.
It does not convert arbitrary printed Lean goals into compatible graphs.
The optional `accepted_local_cues` profile requires normalized goal/hypothesis
records; base inference keeps those runtime-only cues off.

## Reproducibility and limitations

`bundle.json` binds every file. Retrieval validates tower/tokenizer/corpus hashes,
the ID/name population and equality of FAISS rows with the vector matrix.
No training-machine paths or optimizer checkpoints are needed for loading.
Source-code/dependency versions and training stages are in `provenance/`.
The implementation's separate GPLv2 code license is described in `NOTICE`.
Stage diagnostics are in `evaluation/`; their cohorts differ and they are not
a re-evaluation of this whole export. This is an offline experimental system,
not a measured whole-theorem prover or a model trained on the newer template
representations. Live normalized-state serving parity remains a separate gate.
Pin a release tag or full Hugging Face commit for reproducible downloads.