How to use YuxuanGong/lean-RAG with sentence-transformers:
from sentence_transformers import SentenceTransformer model = SentenceTransformer("YuxuanGong/lean-RAG") sentences = [ "theorem length_take_of_le_length | (s.take n).length = n", "Keywords: less than or equal find if and only natural number lemma proposition | Name: Nat le_find_iff | Kind: lemma | Namespace: Nat", "Keywords: length take le' list theorem proposition | Name: List length_take_le' | Kind: theorem | Namespace: List", "Keywords: take length list theorem proposition | Name: List take_length | Kind: theorem | Namespace: List" ] embeddings = model.encode(sentences) similarities = model.similarity(embeddings, embeddings) print(similarities.shape) # [4, 4]
