Lean4-helper / data /mathlib_index
77.3 MB
p4r5kpftnp-cmd
Swap MiniLM retriever for LeanDojo's ByT5 premise encoder
d05440d