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
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.