This release adds a reranker tier and the DeepMind formal-conjectures corpus, and moves the Lean toolchain to 4.31.0.
Highlights
- jina-reranker-v3 optional reranker tier — opt in via
MATHLAS_RERANK_MODELfor a higher-precision second-stage ranking on top of dense retrieval. - DeepMind formal-conjectures corpus ingestion — 3,941 Lean statements plus the FC100 benchmark subsets, folded into the search index.
- numpy 2.4 quantized-tier fix — the int8/binary quantized serving path works again under numpy 2.4; the regression suite grows from 111 to 120 passing.
- Lean 4.30 → 4.31.0 — verification runs against the current toolchain; RESULTS.md suite count refreshed to 120 passed / 2 skipped on Lean 4.31.0, and a verified elan/Lean 4.31.0 setup one-liner is documented.
Docs & packaging
- README positioning pass: validated-writeback RAG framing, AlphaProof Nexus context, and Matlas disambiguation; the formal-conjectures corpus size (3,941 statements) is now noted.
- Hugging Face corpus documented; dataset badge fixed.
- Auto-updating GitHub–Zenodo DOI badge (always shows the live latest DOI); CHANGELOG sorted under per-version headers.