### Generation with timing example

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/api-reference/inference.md

Complete example from README.md:156-162 that times the generation process. Starts a timer, calls model.generate with max_new_tokens=8192, decodes the outputs, and prints both the decoded result and the elapsed time.

```python
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)
```

--------------------------------

### Example of using exfalso to prove a vacuously true statement

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

A Lean 4 example from an earlier version of CombiBench (Liu et al., 2025), which has been corrected in the latest release. It defines functions appears and ubiquitous for binary sequences.

```lean4
import Mathlib

def appears (W: **Z** → Fin 2) (U: Σ n, Fin n → Fin 2) : Prop := ∃ k, ∀ i: Fin U.1, U.2 i = W (k + i)

def ubiquitous (W: **Z** → Fin 2) (U: Σ n, Fin n → Fin 2) : Prop := appears W ⟨U.1 + 1, Fin.snoc U.2 0⟩ ∧ appears W ⟨U.1 + 1, Fin.snoc U.2 1⟩ ∧ appears W ⟨U.1 + 1, Fin.cons 0 U.2⟩ ∧ appears W ⟨U.1 + 1, Fin.cons 1 U.2⟩
```

--------------------------------

### Load tokenizer with AutoTokenizer.from_pretrained

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/api-reference/model-loading.md

Loads the tokenizer for the specified model ID. The example sets a manual seed and uses the 'DeepSeek-Prover-V2-7B' model ID, with an alternative 'DeepSeek-Prover-V2-671B' noted. No additional arguments are passed.

```python
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)
```

--------------------------------

### Generate Lean 4 proof with DeepSeek-Prover-V2 using Transformers

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/README.md

Loads a DeepSeek-Prover-V2 model (7B or 671B) with Hugging Face Transformers, formats a formal Lean 4 statement from miniF2F, and generates a proof. Requires PyTorch and a GPU with enough memory for the model. The example sets a manual seed and measures generation time.

```python
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
  sorry
""".strip()

prompt = """
Complete the following Lean 4 code:

```lean4
{}
```

Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()

chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)
```

--------------------------------

### Complete Lean 4 proof for imosl_2011_c6

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

Full Lean 4 proof that derives False from the hypotheses and then uses exfalso to prove the goal. It constructs the necessary inequalities and applies hW' to get a contradiction.

```lean4
theorem imosl_2011_c6 (W : **Z**→Fin2) (n : **N**+) (N : **N**) (hN : 2 ^n.1 <N) (hW : Function.PeriodicW N) (hW' : ∀N' <N, ¬Function.PeriodicW N') : ∃(x : Finn*↩*→(Σk,Fink→Fin2)), (∀i, (xi).1≠0)∧(∀i,ubiquitousW(xi)) := by
  have h_false : False := by
    have h₁ : 0 <N := by
      have h₂ : 2 ^n.1⩾2 ^ 1 := by
        apply Nat.pow_le_pow_of_le_right
        · norm_num
        · have h₃ : n.1⩾1 := by exact Nat.one_le_of_lt n.2
          linarith
      have h₃ : N> 2 ^n.1 := hN
      have h₄ : N> 0 := by linarith
      linarith
    have h₂ : ¬Function.PeriodicW 0 := by
      apply hW' 0 <;> simpa [h₁] using hN
    have h₃ : Function.PeriodicW 0 := by
      intro z
      simp [Function.Periodic]
    exact h₂ h₃
  have h_main : ∃(x : Finn*↩*→(Σk,Fink→Fin2)), (∀i, (xi).1≠0)∧(∀i,ubiquitousW(xi)) := by
    exfalso
    exact h_false
  exact h_main
```

--------------------------------

### LeanProofFile: Lean 4 proof file structure

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/types.md

Shows the file format of every solution in `minif2f-solutions.zip`. Each `<name>.lean` file is a complete, machine-checked Lean 4 proof, with the `by sorry` line replaced by a full proof. The informal statement appears in the `/-- ... -/` doc comment, and proofs call standard Mathlib tactics.

```lean4
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- <informal statement with $...$ LaTeX and "Show that it is …" answer clause> -/
theorem <name> <quantified variables> <hypotheses> : <conclusion> := by
  <verified proof tactics>
```

--------------------------------

### Lean proof for p*q*r - 1 = 3*((p-1)*(q-1)*(r-1))

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

A Lean 4 proof script that proves the identity for integers p, q, r. It uses case analysis on k (the value of p*q*r - 1 divided by 3) and applies tactics like linarith, nlinarith, norm_num, ring_nf, and omega. The proof includes a subcase for k=3 and uses the fact that the absolute value of (q-3) divides 5.

```lean
have h₁₈ : (p,q,r)=(3, 5, 15):=by simp_all[Prod.ext_iff] <;>norm_num<;>linarith exactOr.inrh₁₈ ·*−−Casek=3* have h₁₄ :p*q*r− 1=3*((p− 1)*(q− 1)*(r− 1)):=by ring_nfathk⊢ <;>linarith have h₁₅ :p=2:=by by_contrah₁₅ have h₁₆ :p⩾3:=by by_contrah₁₆ have h₁₇ :p⩽2:=bylinarith have h₁₈ :p=2:=bylinarith contradiction have h₁₉ :q⩾p+1:=bylinarith have h₂₀ :r⩾q+1:=bylinarith have h₂₁ : (p: **Z**)⩾3:=bylinarith have h₂₂ : (q: **Z**)⩾4:=bylinarith have h₂₃ : (r: **Z**)⩾5:=bylinarith have h₂₄ : (p: **Z**)*q⩾3*4:=bynlinarith have h₂₅ : (p: **Z**)*r⩾3*5:=bynlinarith have h₂₆ : (q: **Z**)*r⩾4*5:=bynlinarith have h₂₇ : (p: **Z**)*q*r⩾3*4*5:=bynlinarith have h₂₈ : (p: **Z**)*q*r− 1=3*((p− 1)*(q− 1)*(r− 1)):=bylinarith have h₂₉ : (p: **Z**)⩾3:=bylinarith have h₃₀ : (q: **Z**)⩾4:=bylinarith have h₃₁ : (r: **Z**)⩾5:=bylinarith have h₃₂ : (p: **Z**)*q*r− 1=3*((p− 1)*(q− 1)*(r− 1)):=bylinarith have h₃₃ :False:=by nlinarith[sq_nonneg((p: **Z**) − 2),sq_nonneg((q: **Z**) − 2),sq_nonneg((r: **Z**) − 2), mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₃), mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₄), mul_nonneg(sub_nonneg.mprh₃) (sub_nonneg.mprh₄)] exacth₃₃ have h₁₆ :q=4:=by have h₁₇ :p=2:=bylinarith have h₁₈ : (p: **Z**)*q*r− 1=3*((p− 1)*(q− 1)*(r− 1)):=bylinarith have h₁₉ : (p: **Z**)=2:=bynorm_num[h₁₇] have h₂₀ : (q: **Z**)⩾3:=by by_contrah₂₀ have h₂₁ :q⩽2:=bylinarith have h₂₂ :q=2:=bylinarith have h₂₃ : (p: **Z**)=2:=bynorm_num[h₁₇] have h₂₄ : (q: **Z**)=2:=bynorm_num[h₂₂] have h₂₅ : (r: **Z**)⩾3:=bylinarith norm_num[h₁₇,h₂₂,h₂₃,h₂₄]ath₁₈ <;> (tryomega) <;> (trynlinarith) <;> (try

{ nlinarith[mul_pos(sub_pos.mprh₀.2.1) (sub_pos.mprh₀.2.2)] }) have h₂₁ : (r: **Z**)⩾q+1:=bylinarith have h₂₂ : (q: **Z**)⩾3:=bylinarith have h₂₃ : (p: **Z**)=2:=bynorm_num[h₁₇] have h₂₄ : (p: **Z**)*q*r− 1=3*((p− 1)*(q− 1)*(r− 1)):=bylinarith have h₂₅ : 2*q*r− 1=3*(1*(q− 1)*(r− 1)):=by norm_num[h₁₇,h₁₉]ath₂₄ ⊢ <;>ring_nfath₂₄ ⊢<;>linarith have h₂₆ : 2*q*r− 1=3*((q− 1)*(r− 1)):=by ring_nfath₂₅ ⊢ <;>nlinarith have h₂₇ : 2*q*r− 1=3*(q*r−q−r+1):=by ring_nfath₂₆ ⊢ <;>nlinarith have h₂₈ : 2*q*r− 1=3*q*r− 3*q− 3*r+3:=by ring_nfath₂₇ ⊢ <;>nlinarith have h₂₉ : −q*r+3*q+3*r− 4=0:=by ring_nfath₂₈ ⊢ <;>nlinarith have h₃₀ : (q: **Z**)*r− 3*q− 3*r+4=0:=by ring_nfath₂₉ ⊢ <;>nlinarith have h₃₁ : (q− 3 : **Z**)*(r− 3 : **Z**)=5:=by ring_nfath₃₀ ⊢ <;>nlinarith have h₃₂ : (q: **Z**) − 3=1∧(r: **Z**) − 3=5∨(q: **Z**) − 3=5∧(r: **Z**) − 3=1∨(q: **Z**) − 3=−1∧(r: **Z**) − 3=−5 ∨(q: **Z**) − 3=−5∧(r: **Z**) − 3=−1:=by have h₃₃ : (q: **Z**) − 3=1∨(q: **Z**) − 3=5∨(q: **Z**) − 3=−1∨(q: **Z**) − 3=−5:=by have h₃₄ : (q: **Z**) − 3|5:=by use(r: **Z**) − 3 linarith have h₃₅ : (q: **Z**) − 3=1∨(q: **Z**) − 3=5∨(q: **Z**) − 3=−1∨(q: **Z**) − 3=−5:=by have h₃₆ : (q: **Z**) − 3=1∨(q: **Z**) − 3=5∨(q: **Z**) − 3=−1∨(q: **Z**) − 3=−5:=by rw[←Int.natAbs_dvd_natAbs]ath₃₄ *−−Weusethefactthattheabsolutevalueof(q−3)dividestheabsolutevalueof5* have h₃₇ : ((q: **Z**) − 3).natAbs|5:=by simpa[Int.natAbs]usingh₃₄ *−−Sincethepossibledivisorsof5are1and5,wecheckthecases* have h₃₈ : ((q: **Z**) − 3).natAbs=1∨((q: **Z**) − 3).natAbs=5:=by have h₃₉ : ((q: **Z**) − 3).natAbs|5:=h₃₇ have h₄₀ : ((q: **Z**) − 3).natAbs⩽5:=Nat.le_of_dvd(bydecide)h₃₉ interval_cases((q: **Z**) − 3).natAbs<;>norm_numath₃₉ ⊢<;>omega casesh₃₈ with |inlh₃₈ => have h₄₁ : (q: **Z**) − 3=1∨(q: **Z**) − 3=−1:=by have h₄₂ : ((q: **Z**) − 3).natAbs=1:=h₃₈ have h₄₃ : (q: **Z**) − 3=1∨(q: **Z**) − 3=−1:=by rw[Int.natAbs_eq_iff]ath₄₂ tauto exacth₄₃ casesh₄₁ with |inlh₄₁ => tauto |inrh₄₁ => tauto |inrh₃₈ => have h₄₁ : (q: **Z**) − 3=5∨(q: **Z**) − 3=−5:=by have h₄₂ : ((q: **Z**) − 3).natAbs=5:=h₃₈
```

--------------------------------

### Lean 4 theorem: induction_ineq_nsqlefactn (complete proof)

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

Provides the complete formal proof of the inequality using induction, with base case and inductive step filled in. The proof uses 'simp' and 'nlinarith' tactics.

```lean4
theorem induction_ineq_nsqlefactn (n : ℕ) (h₀ : 4 ≤ n) : n ^ 2 ≤ n ! := by
  have base_case : 4 ^ 2 ≤ 4 ! := by simp [Nat.factorial]
  have inductive_step : ∀ k ≥ 4, k ^ 2 ≤ k ! → (k + 1) ^ 2 ≤ (k + 1) ! := by
    intro k h₁ h₂
    simp_all [Nat.factorial]
    nlinarith
  have final_proof : ∀ n ≥ 4, n ^ 2 ≤ n ! := by
    intro n hn
    induction' hn with k hk
    case refl => exact base_case
    case step =>
      apply inductive_step k hk
      exact by assumption
  apply final_proof
  exact h₀
```

--------------------------------

### Lean 4 proof attempt with 'have' statements (continued)

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

Continuation of the Lean 4 proof attempt, deriving bounds on r and q using linarith and by_contra.

```lean4
have h₄ : r⩾4:=by by_contra h have h₅ : r⩽3:=by linarith have h₆ : r⩾3:=by linarith[h₀.2.2] have h₇ : r=3:=by linarith have h₈ : q< 3:=by linarith[h₀.2.2] have h₉ : q⩾3:=by linarith[h₃] linarith
```

--------------------------------

### Encoding a single problem statement (README.md:151-156)

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/api-reference/inference.md

Example of encoding a single problem statement: builds a chat list with one user turn and applies the chat template with the same parameters, moving the result to the model device.

```python
chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]
inputs = tokenizer.apply_chat_template(
    chat,
    tokenize=True,
    add_generation_prompt=True,
    return_tensors="pt",
).to(model.device)
```

--------------------------------

### Load 671B variant with failure handling

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/api-reference/model-loading.md

Loads the 671B model variant with the same parameters as the 7B example, but wraps the calls in a try-except block. The repository does not define custom error classes; exceptions come from upstream transformers/huggingface_hub/torch. The guard re-raises a RuntimeError with the model ID.

```python
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "DeepSeek-Prover-V2-671B"

try:
    tokenizer = AutoTokenizer.from_pretrained(model_id)
    model = AutoModelForCausalLM.from_pretrained(
        model_id,
        device_map="auto",
        torch_dtype=torch.bfloat16,
        trust_remote_code=True,
    )
except Exception as exc:
    # Exception classes here belong to transformers / huggingface_hub / torch.
    # The repository does not define or document a specific error contract.
    raise RuntimeError(f"failed to load {model_id}: {exc}") from exc
```

--------------------------------

### Lean 4 proof for k=3 case

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

A Lean 4 proof script for the k=3 case, using tactics like linarith, omega, nlinarith, and ring_nf. It includes case analysis on divisors of 11 and concludes with q=5 and r=15.

```lean
linarith
haveh₄₈ : 2*q+2*r=3:=bylinarith haveh₄₉ : (q: **Z**)⩾3:=byomega haveh₅₀ : (r: **Z**)⩾4:=byomega haveh₅₁ : 2*q+2*r⩾14:=by nlinarith linarith exacth₃₈ haveh₁₉ :q⩾p+1:=byomega haveh₂₀ :r⩾q+1:=byomega haveh₂₁ : (p: **Z**)⩾4:=byomega haveh₂₂ : (q: **Z**)⩾5:=byomega haveh₂₃ : (r: **Z**)⩾6:=byomega haveh₂₄ : (p: **Z**)*q⩾4*5:=bynlinarith haveh₂₅ : (p: **Z**)*r⩾4*6:=bynlinarith haveh₂₆ : (q: **Z**)*r⩾5*6:=bynlinarith haveh₂₇ : (p: **Z**)*q*r⩾4*5*6:=bynlinarith haveh₂₈ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₂₉ : (p: **Z**)⩾4:=byomega haveh₃₀ : (q: **Z**)⩾5:=byomega haveh₃₁ : (r: **Z**)⩾6:=byomega haveh₃₂ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₃₃ :False:=by nlinarith[sq_nonneg((p: **Z**) − 2),sq_nonneg((q: **Z**) − 2),sq_nonneg((r: **Z**) − 2), mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₃), mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₄), mul_nonneg(sub_nonneg.mprh₃) (sub_nonneg.mprh₄)] exacth₃₃ haveh₁₆ :q=5:=by haveh₁₇ :p=3:=bylinarith haveh₁₈ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₁₉ : (p: **Z**)=3:=bynorm_num[h₁₇] haveh₂₀ : (q: **Z**)⩾4:=by by_contrah₂₀ haveh₂₁ :q⩽3:=bylinarith haveh₂₂ :q=3:=bylinarith haveh₂₃ : (p: **Z**)=3:=bynorm_num[h₁₇] haveh₂₄ : (q: **Z**)=3:=bynorm_num[h₂₂] haveh₂₅ : (r: **Z**)⩾4:=bylinarith norm_num[h₁₇,h₂₂,h₂₃,h₂₄]ath₁₈ <;> (tryomega) <;> (trynlinarith) <;> (try { nlinarith[mul_pos(sub_pos.mprh₀.2.1) (sub_pos.mprh₀.2.2)] }) haveh₂₁ : (r: **Z**)⩾q+1:=bylinarith haveh₂₂ : (q: **Z**)⩾4:=bylinarith haveh₂₃ : (p: **Z**)=3:=bynorm_num[h₁₇] haveh₂₄ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₂₅ : 3*q*r− 1=2*(2*(q− 1)*(r− 1)):=by norm_num[h₁₇,h₁₉]ath₂₄ ⊢ <;>ring_nfath₂₄ ⊢<;>linarith haveh₂₆ : 3*q*r− 1=4*((q− 1)*(r− 1)):=by ring_nfath₂₅ ⊢ <;>nlinarith haveh₂₇ : 3*q*r− 1=4*(q*r−q−r+1):=by ring_nfath₂₆ ⊢ <;>nlinarith haveh₂₈ : 3*q*r− 1=4*q*r− 4*q− 4*r+4:=by

ring_nfath₂₇ ⊢

<;>nlinarith haveh₂₉ : −q*r+4*q+4*r− 5=0:=by ring_nfath₂₈ ⊢ <;>nlinarith haveh₃₀ : (q: **Z**)*r− 4*q− 4*r+5=0:=by ring_nfath₂₉ ⊢ <;>nlinarith haveh₃₁ : (q− 4 : **Z**)*(r− 4 : **Z**)=11:=by ring_nfath₃₀ ⊢ <;>nlinarith haveh₃₂ : (q: **Z**) − 4=1∧(r: **Z**) − 4=11∨(q: **Z**) − 4=11∧(r: **Z**) − 4=1∨(q: **Z**) − 4=−1∧(r: **Z**) − 4= −11∨(q: **Z**) − 4=−11∧(r: **Z**) − 4=−1:=by haveh₃₃ : (q: **Z**) − 4=1∨(q: **Z**) − 4=11∨(q: **Z**) − 4=−1∨(q: **Z**) − 4=−11:=by haveh₃₄ : (q: **Z**) − 4|11:=by use(r: **Z**) − 4 linarith haveh₃₅ : (q: **Z**) − 4=1∨(q: **Z**) − 4=11∨(q: **Z**) − 4=−1∨(q: **Z**) − 4=−11:=by haveh₃₆ : (q: **Z**) − 4=1∨(q: **Z**) − 4=11∨(q: **Z**) − 4=−1∨(q: **Z**) − 4=−11:=by rw[←Int.natAbs_dvd_natAbs]ath₃₄ *−−Weusethefactthattheabsolutevalueof(q−4)dividestheabsolutevalueof11* haveh₃₇ : ((q: **Z**) − 4).natAbs|11:=by simpa[Int.natAbs]usingh₃₄ *−−Sincethepossibledivisorsof11are1and11,wecheckthecases* haveh₃₈ : ((q: **Z**) − 4).natAbs=1∨((q: **Z**) − 4).natAbs=11:=by haveh₃₉ : ((q: **Z**) − 4).natAbs|11:=h₃₇ haveh₄₀ : ((q: **Z**) − 4).natAbs⩽11:=Nat.le_of_dvd(bydecide)h₃₉ interval_cases((q: **Z**) − 4).natAbs<;>norm_numath₃₉ ⊢<;>omega casesh₃₈ with |inlh₃₈ => haveh₄₁ : (q: **Z**) − 4=1∨(q: **Z**) − 4=−1:=by haveh₄₂ : ((q: **Z**) − 4).natAbs=1:=h₃₈ haveh₄₃ : (q: **Z**) − 4=1∨(q: **Z**) − 4=−1:=by rw[Int.natAbs_eq_iff]ath₄₂ tauto exacth₄₃ casesh₄₁ with |inlh₄₁ => tauto |inrh₄₁ => tauto |inrh₃₈ => haveh₄₁ : (q: **Z**) − 4=11∨(q: **Z**) − 4=−11:=by haveh₄₂ : ((q: **Z**) − 4).natAbs=11:=h₃₈ haveh₄₃ : (q: **Z**) − 4=11∨(q: **Z**) − 4=−11:=by rw[Int.natAbs_eq_iff]ath₄₂ tauto exacth₄₃ casesh₄₁ with |inlh₄₁ => tauto |inrh₄₁ => tauto exacth₃₆ exacth₃₅ casesh₃₃ with |inlh₃₃ => haveh₃₄ : (q: **Z**) − 4=1:=h₃₃ haveh₃₅ : (r: **Z**) − 4=11:=by haveh₃₆ : ((q: **Z**) − 4)*((r: **Z**) − 4)=11:=by linarith

rw[h₃₄]ath₃₆ linarith exactOr.inl⟨h₃₄,h₃₅⟩ |inrh₃₃ => casesh₃₃ with |inlh₃₃ => haveh₃₄ : (q: **Z**) − 4=11:=h₃₃ haveh₃₅ : (r: **Z**) − 4=1:=by haveh₃₆ : ((q: **Z**) − 4)*((r: **Z**) − 4)=11:=by linarith rw[h₃₄]ath₃₆ linarith exactOr.inr(Or.inl⟨h₃₄,h₃₅⟩) |inrh₃₃ => casesh₃₃ with |inlh₃₃ => haveh₃₄ : (q: **Z**) − 4=−1:=h₃₃ haveh₃₅ : (r: **Z**) − 4=−11:=by haveh₃₆ : ((q: **Z**) − 4)*((r: **Z**) − 4)=11:=by linarith rw[h₃₄]ath₃₆ linarith exactOr.inr(Or.inr(Or.inl⟨h₃₄,h₃₅⟩)) |inrh₃₃ => haveh₃₄ : (q: **Z**) − 4=−11:=h₃₃ haveh₃₅ : (r: **Z**) − 4=−1:=by haveh₃₆ : ((q: **Z**) − 4)*((r: **Z**) − 4)=11:=by linarith rw[h₃₄]ath₃₆ linarith exactOr.inr(Or.inr(Or.inr⟨h₃₄,h₃₅⟩)) rcasesh₃₂ with(⟨h₃₂,h₃₃⟩|⟨h₃₂,h₃₃⟩|⟨h₃₂,h₃₃⟩|⟨h₃₂,h₃₃⟩) ·*−−Case1:q−4=1andr−4=11* haveh₃₄ :q=5:=by linarith haveh₃₅ :r=15:=by linarith simp[h₃₄,h₃₅,h₁₅] <;>norm_num<;>omega ·*−−Case2:q−4=11andr−4=1* haveh₃₄ :q=15:=by linarith haveh₃₅ :r=5:=by linarith haveh₃₆ :r>q:=by linarith linarith ·*−−Case3:q−4=−1andr−4=−11* haveh₃₄ :q=3:=by linarith haveh₃₅ :r=−7:=by linarith haveh₃₆ :r>q:=by linarith linarith ·*−−Case4:q−4=−11andr−4=−1* haveh₃₄ :q=−7:=by linarith haveh₃₅ :r=3:=by linarith haveh₃₆ :r>q:=by
```

--------------------------------

### Load model and generate proof with AutoModelForCausalLM

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/_autodocs/api-reference/model-loading.md

Loads the 7B model variant with device_map='auto', torch_dtype=torch.bfloat16, and trust_remote_code=True. Then applies the chat template, generates up to 8192 new tokens, and decodes the outputs. The model's device is used to move inputs.

```python
model = AutoModelForCausalLM.from_pretrained(
    model_id,
    device_map="auto",
    torch_dtype=torch.bfloat16,
    trust_remote_code=True,
)
inputs = tokenizer.apply_chat_template(chat, tokenize=True,
                                       add_generation_prompt=True,
                                       return_tensors="pt").to(model.device)
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
```

--------------------------------

### Lean proof for k=3 case using nlinarith and linarith

Source: https://github.com/deepseek-ai/deepseek-prover-v2/blob/main/DeepSeek_Prover_V2.pdf

This snippet is a Lean proof for the case k=3, using tactics like nlinarith, linarith, and omega to handle arithmetic reasoning. It includes hypotheses and contradictions to complete the proof.

```lean
nlinarith
haveh₁₈ : (p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**)⩾6:=by nlinarith haveh₁₉ : (k: **Z**)*((p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**))⩾4*((p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**)):=by nlinarith haveh₂₀ : (p*q*r− 1 : **Z**)⩾4*((p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**)):=by linarith haveh₂₁ : (p*q*r− 1 : **Z**) < 4*((p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**)):=by haveh₂₂ : (p: **Z**)*q*r< 4*((p− 1 : **Z**)*(q− 1 : **Z**)*(r− 1 : **Z**))+1:=by nlinarith[mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₃), mul_nonneg(sub_nonneg.mprh₂) (sub_nonneg.mprh₄), mul_nonneg(sub_nonneg.mprh₃) (sub_nonneg.mprh₄)] linarith linarith haveh₁₃ :k=1∨k=2∨k=3:=by omega *−−Weneedtohandleeachcaseofkseparately* rcasesh₁₃ with(rfl|rfl|rfl) ·*−−Casek=1* haveh₁₄ :p*q*r− 1=(p− 1)*(q− 1)*(r− 1):=by ring_nfathk⊢ <;>linarith haveh₁₅ :p*q+p*r+q*r=p+q+r:=by haveh₁₅₁ :p*q*r− 1=(p− 1)*(q− 1)*(r− 1):=bylinarith ring_nfath₁₅₁ ⊢ nlinarith haveh₁₆ :p=2:=by by_contrah₁₆ haveh₁₇ :p⩾3:=by by_contrah₁₇ haveh₁₈ :p⩽2:=bylinarith haveh₁₉ :p=2:=bylinarith contradiction haveh₂₀ :q⩾3:=bylinarith haveh₂₁ :r⩾4:=bylinarith haveh₂₂ : (p: **Z**)*q⩾3*3:=by nlinarith haveh₂₃ : (p: **Z**)*r⩾3*4:=by nlinarith haveh₂₄ : (q: **Z**)*r⩾3*4:=by nlinarith nlinarith haveh₁₇ :q=3:=by by_contrah₁₇ haveh₁₈ :q⩾4:=by by_contrah₁₈ haveh₁₉ :q⩽3:=bylinarith haveh₂₀ :q=3:=bylinarith contradiction haveh₂₁ :p=2:=bylinarith haveh₂₂ : (p: **Z**)*q⩾2*4:=by nlinarith haveh₂₃ : (p: **Z**)*r⩾2*4:=by nlinarith haveh₂₄ : (q: **Z**)*r⩾4*4:=by nlinarith nlinarith haveh₁₈ :r=4:=by by_contrah₁₈ haveh₁₉ :r⩾5:=by by_contrah₁₉

haveh₂₀ :r⩽4:=bylinarith haveh₂₁ :r=4:=bylinarith contradiction haveh₂₂ :p=2:=bylinarith haveh₂₃ :q=3:=bylinarith haveh₂₄ : (p: **Z**)*q⩾2*3:=by nlinarith haveh₂₅ : (p: **Z**)*r⩾2*5:=by nlinarith haveh₂₆ : (q: **Z**)*r⩾3*5:=by nlinarith nlinarith exfalso norm_num[h₁₆,h₁₇,h₁₈]ath₁₄ h₁₅ hkh₀ ⊢<;>linarith ·*−−Casek=2* haveh₁₄ :p*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=by ring_nfathk⊢ <;>linarith haveh₁₅ :p=3:=by by_contrah₁₅ haveh₁₆ :p≠3:=bytauto *−−Weneedtoshowthatpcannotbegreaterthan3* haveh₁₇ :p⩾4:=by by_contrah₁₇ haveh₁₈ :p⩽3:=bylinarith haveh₁₉ :p=2:=by by_contrah₁₉ haveh₂₀ :p⩾3:=byomega haveh₂₁ :p=3:=byomega contradiction haveh₂₂ :p=2:=byomega haveh₂₃ :q⩾3:=bylinarith haveh₂₄ :r⩾4:=bylinarith haveh₂₅ : (p: **Z**)*q⩾2*3:=bynlinarith haveh₂₆ : (p: **Z**)*r⩾2*4:=bynlinarith haveh₂₇ : (q: **Z**)*r⩾3*4:=bynlinarith haveh₂₈ : (p: **Z**)*q*r⩾2*3*4:=bynlinarith haveh₂₉ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₃₀ : (p: **Z**)=2:=byomega haveh₃₁ : (q: **Z**)⩾3:=byomega haveh₃₂ : (r: **Z**)⩾4:=byomega haveh₃₃ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₃₄ : (p: **Z**)=2:=byomega haveh₃₅ : (q: **Z**)⩾3:=byomega haveh₃₆ : (r: **Z**)⩾4:=byomega haveh₃₇ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₃₈ :False:=by haveh₃₉ : (p: **Z**)=2:=byomega haveh₄₀ : (q: **Z**)⩾3:=byomega haveh₄₁ : (r: **Z**)⩾4:=byomega haveh₄₂ : (p: **Z**)*q*r− 1=2*((p− 1)*(q− 1)*(r− 1)):=bylinarith haveh₄₃ : 2*q*r− 1=2*(1*(q− 1)*(r− 1)):=by simp[h₃₉]ath₄₂ ⊢ <;>ring_nfath₄₂ ⊢<;>linarith haveh₄₄ : 2*q*r− 1=2*((q− 1)*(r− 1)):=by ring_nfath₄₃ ⊢<;>linarith haveh₄₅ : 2*q*r− 1=2*(q*r−q−r+1):=by ring_nfath₄₄ ⊢<;>linarith haveh₄₆ : 2*q*r− 1=2*q*r− 2*q− 2*r+2:=by ring_nfath₄₅ ⊢<;>linarith haveh₄₇ : −1=−2*q− 2*r+2:=by
```