Hugging Face's logo

Spaces:
Ray5th
/
Lean4-helper
Running

App Files Community
p4r5kpftnp-cmd Claude Sonnet 4.6 commited on
Commit
cb30699
·
1 Parent(s): 41f9289

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

Browse files

Built locally with: python3 scripts/build_index.py
Mathlib v4.8.0 source extracted via lean-interact cache.

Index files are tracked via Git LFS (index.faiss is 174MB,
index.pkl is 42MB). HF Spaces supports LFS so the Space will
pull these on build.

With the index present, the retriever no longer logs the
"skipping RAG" warning and proofs benefit from retrieved
Mathlib lemma context.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Files changed (3) hide show
  1. .gitattributes +2 -0
  2. data/mathlib_index/index.faiss +3 -0
  3. data/mathlib_index/index.pkl +3 -0
.gitattributes ADDED
@@ -0,0 +1,2 @@
 
 
 
1
+ data/mathlib_index/index.faiss filter=lfs diff=lfs merge=lfs -text
2
+ data/mathlib_index/index.pkl filter=lfs diff=lfs merge=lfs -text
data/mathlib_index/index.faiss ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:68909be7e23f6ee5ce10beb50aab83f384ad0a528e2b85834e78e05c9fa47d3b
3
+ size 182607405
data/mathlib_index/index.pkl ADDED
@@ -0,0 +1,3 @@
 
 
 
 
1
+ version https://git-lfs.github.com/spec/v1
2
+ oid sha256:f46ec4dffba8f1fd2f7e1d917eea32fb9bf272cb7684e40820860d56f11d52dd
3
+ size 44132895