Upload README.md

README.md

@@ -0,0 +1,41 @@
+Usage:
+
+```python
+import torch
+from transformers import AutoTokenizer, AutoModelForCausalLM
+
+question_template = "<|im_start|>user\nMy LEAN 4 state is:\n```{state}```\nPlease write down the reasoning that leads to the possible next tactic and then predict the tactic to help me prove the theorem.<|im_end|>\n<|im_start|>assistant\n"
+
+model_name = "ScalableMath/Lean-STaR-plus"
+model = AutoModelForCausalLM.from_pretrained(model_name, torch_dtype=torch.bfloat16, device_map="auto")
+
+tokenizer = AutoTokenizer.from_pretrained(model_name)
+
+state = "x : \u211d\nn : \u2115\nh\u2080 : -1 < x\nh\u2081 : 0 < n\n\u22a2 1 + \u2191n * x \u2264 (1 + x) ^ n"
+question = question_template.format(state=state)
+
+input_tensor = torch.tensor([tokenizer.encode(question)])
+outputs = model.generate(input_tensor.to(model.device), max_new_tokens=500)
+
+result = tokenizer.decode(outputs[0], skip_special_tokens=True)
+print(result)
+```
+
+Example Results:
+```
+# State
+
+x : ℝ
+n : ℕ
+h₀ : -1 < x
+h₁ : 0 < n
+⊢ 1 + ↑n * x ≤ (1 + x) ^ n
+
+# Reasoning
+
+To prove the inequality involving the binomial expansion of `(1 + x)^n`, we start by considering the binomial expansion of `1 + x` raised to the power `n`. This expansion will allow us to compare the left-hand side and the right-hand side of the inequality.
+
+# Next Tactic
+
+have h₂ : x = -1 + (x + 1) := by simp
+```