How to use ruc-ai4math/Lean_State_Search_Random with Transformers:
# Load model directly from transformers import AutoModel model = AutoModel.from_pretrained("ruc-ai4math/Lean_State_Search_Random", dtype="auto")