StepFun-Prover-Preview-32B

from vllm import LLM, SamplingParams
from transformers import AutoTokenizer

model_name = "Stepfun/Stepfun-Prover-Preview-32B"
model = LLM(
    model=model_name,
    tensor_parallel_size=8,
    )
tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True)

formal_problem = """
import Mathlib

theorem test_theorem (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
    (x^2 - z^2) / (y + z) + (y^2 - x^2) / (z + x) + (z^2 - y^2) / (x + y) ≥ 0 := by
""".strip()

system_prompt = "You will be given an unsolved Lean 4 problem. Think carefully and work towards a solution. At any point, you may use the Lean 4 REPL to check your progress by enclosing your partial solution between <sketch> and </sketch>. The REPL feedback will be provided between <REPL> and </REPL>. Continue this process as needed until you arrive at a complete and correct solution."

user_prompt = f"