ScalableMath/Lean-STaR-plus

Usage:

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