Spaces:

Ray5th
/

Lean4-helper

Running

App Files Files Community

Lean4-helper / data /mathlib_index /index.faiss

Commit History

Swap MiniLM retriever for LeanDojo's ByT5 premise encoder

d05440d

p4r5kpftnp-cmd commited on Jun 4

Add pre-built Mathlib FAISS index (118,885 declarations)

cb30699

p4r5kpftnp-cmd Claude Sonnet 4.6 commited on May 19