README.md

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

```