DeepSeek-Prover V2

Stream: Machine Learning for Theorem Proving

[Andy Jiang]

Looks like Deepseek's new model set a new record on PutnamBench ->https://x.com/zhs05232838/status/1917600755936018715

[George Tsoukalas]

49 problems solved is a huge improvement over previous bests. I've reached out to the DeepSeek team so they can send me the proofs to validate, so I can add the model to the leaderboard. (Though I only sent to their service email, if any members of the team see this, reach out!)

[Auguste Poiroux]

I like the super long Lean proof starting page 23 and ending page 32 of the report :exploding_head:

[Floris van Doorn]

It has certainly learned how to break proofs into small steps!

[...]
have h30 : (p : Z) = 2 := by omega
have h31 : (q : Z) ⩾ 3 := by omega
have h32 : (r : Z) ⩾ 4 := by omega
have h33 : (p : Z) * q * r − 1 = 2 * ((p − 1) * (q − 1) * (r − 1)) := by linarith
have h34 : (p : Z) = 2 := by omega
have h35 : (q : Z) ⩾ 3 := by omega
have h36 : (r : Z) ⩾ 4 := by omega
have h37 : (p : Z) * q * r − 1 = 2 * ((p − 1) * (q − 1) * (r − 1)) := by linarith
have h38 : False := by
  have h39 : (p : Z) = 2 := by omega
  have h40 : (q : Z) ⩾ 3 := by omega
  have h41 : (r : Z) ⩾ 4 := by omega
[...]

[Floris van Doorn]

But joking aside, the performance and these formal proofs look impressive! That is very different than some of the previous proofs that some models gave, which basically felt like "we learned how to provide 2 useful arguments to nlinarith".

[Jason Rute]

Maybe this should be its own topic?

[Notification Bot]

6 messages were moved here from #Machine Learning for Theorem Proving > PutnamBench by Floris van Doorn.

[Jason Rute]

This is impressive work! I look forward to understanding it better, especially in relation to the recent Kimina work.

[Joseph Myers]

Does validation for PutnamBench include making sure that the proofs do solve the intended informal problem (rather than showing up incorrect formal statements in the benchmark)?

The report also refers to solving 12 problems from CombiBench, which even more needs assessment of whether those problems have correct formal statements.

[Joseph Myers]

Given this work, does DeepSeek intend to make formal-to-formal attempts at the problems from the next few IMOs, Putnams etc. when they come out (preferably with independent formal statements shared between all AIs making such attempts for better comparability than each AI having its own Lean versions of the problems)?

[Li Xuanji]

One unfortunate thing I noticed from the paper is that it's evaluated using Lean 4.9 (which was released last July) and benchmark problems which are incompatible with Lean 4.9 are excluded. It's not clear to me whether this is due to model limitations or for better testing control (since DeepSeek-Prover-1.5 is also evaluated with Lean 4.9)

[Alok Singh]

Li Xuanji said:

One unfortunate thing I noticed from the paper is that it's evaluated using Lean 4.9 (which was released last July) and benchmark problems which are incompatible with Lean 4.9 are excluded. It's not clear to me whether this is due to model limitations or for better testing control (since DeepSeek-Prover-1.5 is also evaluated with Lean 4.9)

I just opened my phone to post the same point, but you were there first

[Kelly Davis]

Jason Rute said:

This is impressive work! I look forward to understanding it better, especially in relation to the recent Kimina work.

They speak a bit to this point in the Cold Start by Synthetic Data subsection of Section 2.2

[Auguste Poiroux]

Li Xuanji said:

One unfortunate thing I noticed from the paper is that it's evaluated using Lean 4.9 (which was released last July) and benchmark problems which are incompatible with Lean 4.9 are excluded. It's not clear to me whether this is due to model limitations or for better testing control (since DeepSeek-Prover-1.5 is also evaluated with Lean 4.9)

I would say it is probably neither about "model limitations" or "better testing control", but just about their technical setup. They are using https://github.com/xinhjBrant/mathlib4/tree/deepseek with a fixed version of a forked REPL. Their tooling and datasets are probably built around that.

[Albert Jiang]

George Tsoukalas said:

49 problems solved is a huge improvement over previous bests. I've reached out to the DeepSeek team so they can send me the proofs to validate, so I can add the model to the leaderboard. (Though I only sent to their service email, if any members of the team see this, reach out!)

Let me ask Zhihong about this.

[Jason Rute]

@Albert Jiang you may want to also point out all the mistakes people found in their benchmark: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/ProverBench/

[Wang Jingting]

Well, I tried the 7B model locally, and it worked really great. But there's something I feel that I have to point out: In the Appendix B of the paper, both of the proofs there has used apply?, and the proof seems not to actually work? (Since aside from apply?, it seems that nothing non-trivial has been proved, so I'm wondering if they have mistaken that as having proved the problem?)

[Jason Rute]

Wang Jingting said:

Well, I tried the 7B model locally, and it worked really great. But there's something I feel that I have to point out: In the Appendix B of the paper, both of the proofs there has used apply?, and the proof seems not to actually work? (Since aside from apply?, it seems that nothing non-trivial has been proved, so I'm wondering if they have mistaken that as having proved the problem?)

I agree it looks wrong. The proof doesn't use most of the assumptions. @George Tsoukalas Please look at this one closely when you get a chance. Is this problem wrong in PutnamBench, or do they have a buggy proof-checking harness? If the latter, I'm worried that their numbers might be much too high due to bugs in their infrastructure.

[Auguste Poiroux]

A wrong apply? proof being accepted closely resembles to the bugs of the tactic mode of the REPL that have been recently fixed (second fix specific to wrong self-application).
However, I would be surprised if they used the REPL tactic mode for DeepSeekProver-V2 given that they only used the command mode for DeepSeek-Prover v1.5 as far as I know. And from what I understand in their DeepSeek-Prover V2 report, they are also very likely using the command mode only.

[Jason Rute]

It would be good to go through their miniF2F solutions and find proofs with apply?. (And also to independently check all their solutions in Lean 4.9 or whatever it is that they use.)

[Mantas Baksys]

There is another Putnam problem using apply? that only formalizes variations of the answer statement in have statements without proof and then uses the final one to close the goal. I am really use about the results of this paper now, I would speculate that their REPL is dodgy and allows for these proofs to pass. Just a quick mention that the Kimina Lean server (https://github.com/project-numina/kimina-lean-server) catches these proofs as incomplete.

[Marco Dos Santos]

Yes, for example the first proof of Appendix B doesn't pass our verification with the Kimina Lean Server:
{'has_error': False, 'is_valid_no_sorry': False, 'is_valid_with_sorry': True}
It is a valid proof, but it counts as a proof using sorry.

[Jason Rute]

This could be really bad for them. Is anyone willing to check all there minif2f results? (They haven’t posted the Putnam bench results yet.)

[Mert Ünsal]

Let me try to validate their MiniF2F using Kimina Lean Server.

[Jason Rute]

(They officially use Lean 4.9 I think, so that may create issues.)

[Pietro Monticone]

I tested both proofs published in Appendix B using Lean v4.9.0 and I can confirm they're both incomplete.

[Auguste Poiroux]

Just checked all their minif2f proofs using LeanInteract with Lean v4.9.0. Unless I made a mistake in my code, no issues to report. They probably just made a mistake in their appendix.

Code

import os
from concurrent.futures import ThreadPoolExecutor, as_completed

from lean_interact import AutoLeanServer, FileCommand, LeanREPLConfig, TempRequireProject
from lean_interact.interface import LeanError

config = LeanREPLConfig(lean_version="v4.9.0", project=TempRequireProject("mathlib"))


# Helper function to process a single file
def process_file(path):
    server = AutoLeanServer(config)
    response = server.run(FileCommand(path=path))
    if isinstance(response, LeanError) or not response.lean_code_is_valid(allow_sorry=False):
        print(f"Error in {path}: {response}")
        return False
    else:
        return True


# run all the lean files inside the `test` and `valid` folders
root_dir = os.path.dirname(os.path.abspath(__file__))
for split in ["test", "valid"]:
    files_to_run = []
    for root, dirs, files in os.walk(os.path.join(root_dir, split)):
        for file in files:
            if file.endswith(".lean"):
                path = os.path.join(root_dir, root, file)
                files_to_run.append(path)

    counter_correct = 0
    counter_total = 0

    with ThreadPoolExecutor() as executor:
        futures = {executor.submit(process_file, path): path for path in files_to_run}
        for future in as_completed(futures):
            counter_total += 1
            if future.result():
                counter_correct += 1
            print(f"Correct: {counter_correct}/{counter_total}")

[Pietro Monticone]

Minor note: there is an apply?-incomplete proof in the valid set.

[Auguste Poiroux]

algebra_amgm_prod1toneq1_sum1tongeqn.lean? It looks ok in the online Lean IDE, although there is a weird message: mathlib-demo.lean:8:0 AddConstAsyncResult.commitConst: constant has level params [u_1] but expected []

[Simon Sorg]

Auguste Poiroux said:

algebra_amgm_prod1toneq1_sum1tongeqn.lean? It looks ok in the online Lean IDE, although there is a weird message: mathlib-demo.lean:8:0 AddConstAsyncResult.commitConst: constant has level params [u_1] but expected []

One of the messages is declaration uses 'sorry'

[Auguste Poiroux]

Yes indeed, I read apply? as exact? in my head. Sorry for the confusion

[Auguste Poiroux]

Well, then it seems that the REPL is not reporting this declaration uses 'sorry' message. This might be the real issue here. Thanks for reporting this @Pietro Monticone.

[Deming Xu]

https://huggingface.co/playground
https://openrouter.ai/chat

I found this model (deepseek-ai/DeepSeek-Prover-V2-671B) on Hugging Face Playground and OpenRouter! Hugging Face Playground should support free use of this model online. It seems like unlike previous Lean models, the API providers decided to add support for this one.

[Deming Xu]

I ran these tests:

import Mathlib.Tactic
import Mathlib.Data.Real.Basic


/--
Formalize and prove this in Lean:

"A implies B", if and only if "either not A or B"
-/
theorem imp_iff_not_or' (A B : Prop) : (A → B) ↔ (¬ A ∨ B) := by
  apply Iff.intro
  · -- Prove the forward direction: (A → B) → (¬ A ∨ B)
    intro h
    by_cases hA : A
    · -- Case: A is true
      have hB : B := h hA
      exact Or.inr hB
    · -- Case: A is false
      exact Or.inl hA
  · -- Prove the backward direction: (¬ A ∨ B) → (A → B)
    intro h
    intro hA
    cases h with
    | inl hnA =>
      -- Case: ¬ A is true
      exfalso
      exact hnA hA
    | inr hB =>
      -- Case: B is true
      exact hB

/--
Formalize and prove this in Lean:

For a real number x != 0, abs(x + 1/x) >= 2
-/
theorem abs_x_plus_inv_x_ge_two (x : ℝ) (hx : x ≠ 0) : |x + 1 / x| ≥ 2 := by
  have h₁ : (x + 1 / x) ^ 2 ≥ 4 := by
    have h₂ : (x - 1 / x) ^ 2 ≥ 0 := by nlinarith
    calc
      (x + 1 / x) ^ 2 = (x - 1 / x) ^ 2 + 4 := by
        -- Prove that (x + 1/x)^2 = (x - 1/x)^2 + 4
        field_simp [hx]
        ring
        <;>
        nlinarith
      _ ≥ 0 + 4 := by nlinarith
      _ = 4 := by norm_num
  -- Now we know (x + 1/x)^2 ≥ 4, so |x + 1/x| ≥ 2
  have h₂ : |x + 1 / x| ≥ 2 := by
    -- Use the fact that if y^2 ≥ 4, then |y| ≥ 2
    have h₃ : (x + 1 / x) ^ 2 ≥ 4 := h₁
    have h₄ : |x + 1 / x| ≥ 2 := by
      -- Use the property of squares and absolute values
      have h₅ : 2 ≤ |x + 1 / x| := by
        by_contra h₅
        -- If |x + 1/x| < 2, then (x + 1/x)^2 < 4
        have h₆ : |x + 1 / x| < 2 := by linarith
        have h₇ : (x + 1 / x) ^ 2 < 4 := by
          calc
            (x + 1 / x) ^ 2 = |x + 1 / x| ^ 2 := by
              -- Since (x + 1/x)^2 = |x + 1/x|^2
              nlinarith [abs_mul_abs_self (x + 1 / x)]
            _ < 2 ^ 2 := by
              gcongr <;> nlinarith
            _ = 4 := by norm_num
        linarith
      linarith
    exact h₄
  exact h₂


/--
Formalize and prove this in Lean:

For a real number b, if there is not x such that
x^2 + b * x + 1 = 0
then abs(b) < 2
-/
theorem no_real_root_implies_abs_lt_two (b : ℝ) : (¬ ∃ (x : ℝ), x^2 + b * x + 1 = 0) → abs b < 2 := by
  intro h
  have h₁ : b^2 - 4 < 0 := by
    by_contra h₂
    -- If b² - 4 ≥ 0, then the quadratic has a real root, contradicting h.
    have h₃ : b^2 - 4 ≥ 0 := by linarith
    have h₄ : ∃ (x : ℝ), x^2 + b * x + 1 = 0 := by
      -- Use the quadratic formula to find a root.
      use (-b + Real.sqrt (b^2 - 4)) / 2
      have h₅ : b^2 - 4 ≥ 0 := by linarith
      have h₆ : Real.sqrt (b^2 - 4) ≥ 0 := Real.sqrt_nonneg (b^2 - 4)
      nlinarith [Real.sq_sqrt (by linarith : 0 ≤ b^2 - 4), sq_nonneg (b - Real.sqrt (b^2 - 4))]
    exact h h₄
  have h₂ : abs b < 2 := by
    -- Prove that |b| < 2 using h₁.
    have h₃ : b^2 < 4 := by linarith
    have h₄ : abs b < 2 := by
      rw [abs_lt]
      constructor <;> nlinarith [sq_nonneg b, sq_nonneg (b - 2), sq_nonneg (b + 2)]
    exact h₄
  exact h₂

/--
Formalize and prove this in Lean:

For a real number x, if x^3 = 8, then x = 2.
-/
theorem cube_root_of_eight (x : ℝ) (h : x^3 = 8) : x = 2 := by
  have h₁ : (x - 2) * (x^2 + 2 * x + 4) = 0 := by
    have h₂ : x^3 - 8 = 0 := by linarith
    have h₃ : x^3 - 8 = (x - 2) * (x^2 + 2 * x + 4) := by ring
    rw [h₃] at h₂
    exact h₂
  have h₂ : x - 2 = 0 ∨ x^2 + 2 * x + 4 = 0 := by
    apply eq_zero_or_eq_zero_of_mul_eq_zero h₁
  cases h₂ with
  | inl h₂ =>
    have h₃ : x = 2 := by linarith
    exact h₃
  | inr h₂ =>
    have h₃ : x^2 + 2 * x + 4 = 0 := h₂
    have h₄ : (x + 1)^2 + 3 = 0 := by nlinarith
    have h₅ : False := by nlinarith
    exfalso
    exact h₅

[Deming Xu]

image.png

[Thomas Zhu]

Besides fixing REPL issues of not reporting the sorry, in my opinion the Lean side should also be changed: apply? shouldn't close a goal with sorry if no suggestions close the goal. (This was discussed.)

[Patrick Massot]

I don't think we should make Lean less nice to use for humans for the sake of agents. There could be an opt-in option for agents though.

[Thomas Zhu]

I think there is some misunderstanding: I am suggesting that making apply? not admit the goal when no suggestions close the goal is beneficial both for human users and for LLMs. At least this is the impression I got from this thread and my linked thread.

[Eric Wieser]

Why is having tactics use sorry a problem?

[Auguste Poiroux]

Auguste Poiroux said:

Well, then it seems that the REPL is not reporting this declaration uses 'sorry' message. This might be the real issue here. Thanks for reporting this Pietro Monticone.

Coming back to this, it seems that it's not a REPL issue. In Lean v4.9.0, when apply? is used in a proof we don't get a sorry message. Do any of you know when it was introduced? Additionally, are there other tactics that should be reported as sorry? I will update LeanInteract to check for these tactics when looking for sorries.

[Eric Wieser]

I don't think this is a trustworthy way to determine if a proof is sorry-free (but this is a user-interface bug)

[Jason Rute]

Eric Wieser said:

Why is having tactics use sorry a problem?

For one, it is frustrating to debug. Where did the sorry come from? It isn't like Lean will tell you which tactic was the cause of the sorry. For a novice user, they may not even suspect the ? tactics. The above thread is an example of someone getting confused why apply? closes the goal. Conversely, how does it help for a typical tactic? (Obviously not sorry or a well-known synonym, although I would also love for sorry synonyms to be made more sorry-like in appearance, as well as tactics which introduce sorries, no?). But I'm not a Lean power-user. Is there an advantage to using sorry in this case or similar tactics?

[Eric Wieser]

I think the argument for using sorry is to avoid:

• the user seeing an annoying "unsolved goals" error on a goal they are actively working on
• a warning that the apply? tactic does nothing

[Thomas Zhu]

Eric Wieser said:

I don't think this is a trustworthy way to determine if a proof is sorry-free (but this is a user-interface bug)

This I absolutely agree. Would you say a more future proof way is to check the set of axioms used is a subset of the standard three?

[Auguste Poiroux]

Eric Wieser said:

I don't think this is a trustworthy way to determine if a proof is sorry-free

Well, yes, you are right, I agree with you. A better way would be to enhance the REPL command mode to do an explicit check then. It would probably reuse the getProofStatus method introduced to check proofs in tactic mode. What do you think? I might try to implement that in the coming weeks.

[Pietro Monticone]

The two PutnamBench problems in Appendix B would not compile even without the apply? issue, right?

[Pietro Monticone]

In particular, as far as I can tell,

• putnam_2005_a4 would not compile even if you replaced apply? with sorry. The whole calc block is invalid.
• putnam_2007_b4 doesn’t compile because of an error in the rw preceding the apply?. Do you happen to know why it wasn’t detected?

[Leni Aniva]

Pantograph can check whether there's a sorry immediately after a tactic finishes, so there is that

[Jason Rute]

Can you use pantograph to check proofs like these?

[Leni Aniva]

Jason Rute said:

Can you use pantograph to check proofs like these?

e.g.?

We need to parse these text proofs into a proof tree if you want to do something like that

[Auguste Poiroux]

Pietro Monticone said:

In particular, as far as I can tell,

• putnam_2005_a4 would not compile even if you replaced apply? with sorry. The whole calc block is invalid.
• putnam_2007_b4 doesn’t compile because of an error in the rw preceding the apply?. Do you happen to know why it wasn’t detected?

I don't know what's happening with these PutnamBench proofs, I cannot manage to get them to compile, neither in VSCode or using the REPL...

[Jason Rute]

@Leni Aniva Any of the proofs in: https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

[Eric Wieser]

Surely we should just be checking these proofs with leanchecker + an axioms check?

[Leni Aniva]

Jason Rute said:

Leni Aniva Any of the proofs in: https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

probably not, if you want the precise location of the tactics producing sorrys

[Eric Wieser]

Leni Aniva said:

Pantograph can check whether there's a sorry immediately after a tactic finishes, so there is that

Does it detect

theorem foo : 1 = 0 := by
  let rec bar : 1 = 0 := by apply?
  exact bar

[Leni Aniva]

Eric Wieser said:

Pantogr

Leni Aniva said:

Pantograph can check whether there's a sorry immediately after a tactic finishes, so there is that

Does it detect

theorem foo : 1 = 0 := by
  let rec bar : 1 = 0 := by apply?
  exact bar

Yes, but you would have to run it with goal_tactic (what an agent would call when searching for the proof)

from pantograph.server import Server
from pantograph.expr import TacticHave

if __name__ == '__main__':
    server = Server(imports=['Init'])
    state0 = server.goal_start("1 = 0")
    state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave("1 = 0"))
    print(state1)
    state1b = server.goal_tactic(state1, goal_id=0, tactic="apply?")
    print(state1b)

This fails on line -2.

[Jason Rute]

Eric Wieser said:

Surely we should just be checking these proofs with leanchecker + an axioms check?

Someone needs to write a document for AI researchers telling them about common pitfalls, axioms, checking proofs, errors in benchmarks, and other things which would embarrass them if they don't handle correctly.

[Jason Rute]

(Also because it wastes everyone's time.)

[Auguste Poiroux]

Eric Wieser said:

Leni Aniva said:

Pantograph can check whether there's a sorry immediately after a tactic finishes, so there is that

Does it detect

theorem foo : 1 = 0 := by
  let rec bar : 1 = 0 := by apply?
  exact bar

If we switch to tactic mode, the REPL detect this issue. The output is a bit long, but you get proof_status='Incomplete: contains metavariable(s)'.

Code

from lean_interact import AutoLeanServer, Command, LeanREPLConfig, ProofStep

conf = LeanREPLConfig(lean_version="v4.9.0")
server = AutoLeanServer(conf)

server.run(Command(cmd="theorem foo : 1 = 0 := by sorry"))
response = server.run(
    ProofStep(
        tactic="(\n  let rec bar : 1 = 0 := by apply?\n  exact bar)",
        proof_state=0,
    )
)
print(response)

Output

ProofStepResponse(proof_status='Incomplete: contains metavariable(s)', messages=[Message(data='Try this: refine Nat.eq_zero_of_add_eq_zero_left ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_le_zero ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.le_zero.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_not_pos ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Int.ofNat_eq_zero.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_zero_dvd ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.zero_dvd.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_gcd_eq_zero_left ?H', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_gcd_eq_zero_right ?H', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_zero_of_add_eq_zero_right ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_beq_eq_true ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.le_antisymm ?h₁ ?h₂', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Lean.ofReduceNat 1 0 ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data="Try this: refine Nat.succ_inj'.mp ?a✝", severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.add_right_cancel ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.pred_inj ?a✝ ?a✝¹ rfl', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_mul_eq_mul_left ?hn ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_iff_le_and_ge.mpr ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.add_left_cancel ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_mul_eq_mul_right ?hm ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_lt_succ_of_not_lt ?hmn ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_le_of_lt_succ ?h₁ ?h₂', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.le_antisymm_iff.mpr ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Int.negSucc_inj.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Int.ofNat_inj.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.dvd_antisymm ?a✝ ?a✝¹', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.mul_left_cancel ?np ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.add_right_cancel_iff.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.add_left_cancel_iff.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine (Nat.mul_right_cancel_iff ?p 1 0).mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.mul_right_cancel ?mp ?h', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine (Nat.mul_left_cancel_iff ?p 1 0).mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Fin.mk.inj_iff.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.eq_of_testBit_eq ?pred', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0)), Message(data='Try this: refine Nat.compare_eq_eq.mp ?a✝', severity='info', start_pos=Pos(line=0, column=0), end_pos=Pos(line=0, column=0))], goals=[], proof_state=1)

[Leni Aniva]

There's nothing wrong if a proof step contains mvars. Either the error message is misleading in the repl, or its being overeager in detecting errors.

[Leni Aniva]

Im not familiar with lean_interact. Does this example assume the proof is finished?

[Auguste Poiroux]

Leni Aniva said:

There's nothing wrong if a proof step contains mvars. Either the error message is misleading in the repl, or its being overeager in detecting errors.

The check is for expression metavariables with hasExprMVar

[Leni Aniva]

Auguste Poiroux said:

Leni Aniva said:

There's nothing wrong if a proof step contains mvars. Either the error message is misleading in the repl, or its being overeager in detecting errors.

The check is for expression metavariables with hasExprMVar

so? What Im saying is unless we declare a proof to be fully complete, goals can have mvars, proof terms can have mvars, and these would not be a problem.

[Auguste Poiroux]

Leni Aniva said:

Im not familiar with lean_interact. Does this example assume the proof is finished?

This is not specific to LeanInteract, I am just using it for the interface to the REPL and for using Lean v4.9.0.
This example assume the proof is finished because there are no goals left. But there is a hole, hence the hasExprMvar check that fails

[Notification Bot]

11 messages were moved from this topic to #lean4 > #print axioms does not report sorry by Eric Wieser.

[Jason Rute]

Just so it is clear, that proof of algebra_amgm_prod1toneq1_sum1tongeqn is likely an example of an AI agent finding and exploiting a bug in Lean. The bug is the one mentioned in the above message. Even if DeepSeek were diligent and used #print axioms ... it would not have triggered anything suspicious. (Maybe it is the same with the putnam problems when we see the actual code. That could explain why the agent is using Cardinal.toNat.) If this is the case, this is really interesting and should be made more well known!

[Jason Rute]

(Edit: I'm calling it a bug now, not a "soundness bug".)

[Jason Rute]

(Our graph2tac paper found aN issue, but that was just an axiom of False that didn't take care to check for. This is much more crazy.)

[Patrick Massot]

Jason, I think it would be much wiser to remove that bold sentence and stick to facts.

[Patrick Massot]

This is not at all what people call a soundness bug. This has a precise meaning.

[Jason Rute]

Is the precise meaning based on external checking?

[Jason Rute]

Or the kernel?

[Jason Rute]

Of is #print axioms also part of that?

[Jason Rute]

Because there did seem to be a bug in #print axioms?

[Patrick Massot]

The kernel.

[Jason Rute]

What should I call it? A student could use this same trick to cheat on a Lean assignment (if not using an extenal checker).

[Patrick Massot]

#print axiom is a convenient command to quickly check something is axiom free, and it would indeed be nice to make it more reliable. But this has nothing to do with a soundness bug.

[Patrick Massot]

You can call it a bug in a convenience command.

[Jason Rute]

"Has nothing to do with" is too strong. There is a name for this. Let me look it up.

[Jason Rute]

I thought it was "Pollack consistency" but that is slightly different. Okay, I'll just call it a "bug in Lean".

[Sebastian Ullrich]

I commented on the non-severity in the other thread.

[Patrick Massot]

Jason, you make it sound like the bug in this command is enough, but the main thing is the bug in the AI pipeline that simply doesn’t check the Lean kernel accepts the proof.

[Jason Rute]

My point is this. It is well known you can trick Lean to make a bad proof look right. You can mess with the tactic environment and such. Sure, if you do external proof checking, it would be caught, but 99% of Lean users don't do that. this is a case of an AI agent finding a very subtle bug in Lean such that #print axioms doesn't say sorry is used. I think it is a big deal. Lean's kernel is fine and external type checking still works, but for AI research it isn't enough to rely on Lean's command line + print axioms. You have to export the proofs. Is this balanced and fair?

[Jason Rute]

The bug in the AI pipeline could have just been that they didn't use external type checking.

[Jason Rute]

Oh, I see. I should try to run this proof on the command line. That apparently fails according to @Sebastian Ullrich. Let me do that.

[Luigi Massacci]

Jason Rute said:

The bug in the AI pipeline could have just been that they didn't use external type checking.

Surely this is the most reasonable answer. Besides I'm not sure I agree that 99% of lean users don't know this. Anyone who uses lean mostly as a human will inevitably run into issues like these, and they come up all the time on Zulip. There's plenty of threads suggesting to use done at the end of proofs, etc... I think only people that interact with lean mostly via REPL will not have run into something similar.

[Thomas Zhu]

I think I have to disagree with @Jason Rute here:

1. There are two bugs: a Lean bug of #print axioms and a REPL bug of apply?.
2. I wrote the #print axioms line myself to debug the seeming absence of squiggly lines of apply? (which turned out to be a VS Code issue)
3. #print axioms did break, but as far as I know, #print axioms is not used by DeepSeek's team to check correctness. The agent probably didn't find/exploit whatever bug I found.
4. The original proof in the zip file released by DeepSeek was indeed incorrect, and some bug was exploited by the DeepSeek-Prover-V2 model. But this bug is the apply? bug: it is something like Lean REPL not reporting the sorry warning message in apply? (I have not read all the details above); and I don't have any evidence this apply? issue is at all related to the #print axioms issue. Since this is probably a REPL issue, this should be categorized as a bug in the AI pipeline and not a bug in Lean.
5. DeepSeek-Prover-V2 did not use apply? on any other problem in miniF2F. I think their numbers on miniF2F are still broadly sound (except for this 0.4% difference on miniF2F-valid). But the proofs of PutnamBench should warrant a more detailed check.
6. I would say this "bug discovery" is me trying to debug the apply? issue and (because DeepSeek-Prover-V2 wrote the Type*) accidentally triggering the #print axioms bug during debugging. It's interesting that besides the sorry warning, the AddConstAsyncResult.commitConst: constant has level params [u] but expected [] error message was also not caught by DeepSeek-Prover-V2's checking (perhaps because there is also some message upper limit for REPL like VS Code?) but I don't expect DeepSeek-Prover to have put the Type* there to deliberately trigger the #print axioms bug for humans at all (see Appendix B of their paper).

[Leni Aniva]

Lean doesn't have a single message for "this proof is not correct", and the engineers at DeepSeek did not cover all of the cases where a proof fails. That is my impression about this problem

[Thomas Zhu]

I would say it is impressive that DeepSeek-Prover-V2 cheated their pipeline (perhaps using REPL) of checking proofs. But reward cheating in RL happens all the time: it only takes the agent to write an apply? tactic once to find it.

[Jason Rute]

#print axioms did break, but as far as I know, #print axioms is not used by DeepSeek's team to check correctness. The agent probably didn't find/exploit whatever bug I found.

Maybe. But in that case, I'm surprised apply? wasn't used more by the AI. You could solve everything with it.

[Leni Aniva]

they probably havent trained it enough to collapse its output distribution yet

[Deming Xu]

#lean4 > #print axioms does not report sorry

Just to be clear, you mentioned in that thread that the error will not come up in Lean version 4.18.0, and it might be "an unintended side effect of parallelism", which is probably a new feature? And you mentioned that DeepSeek was using Lean 4.9, so this #print axioms bug itself probably does not affect the DeepSeek team, right?

I tested your code snippet on my machine.

universe u

-- declaration uses 'sorry'
-- AddConstAsyncResult.commitConst: constant has level params [u] but expected []
theorem f : False := by
  let a {α : Type u} : α → α := id
  sorry

-- 'f' does not depend on any axioms
#print axioms f

-- Let's try using this `f`
-- (kernel) unknown constant 'f'
theorem g : 1 + 1 = 3 := False.elim f

When my lean-toolchain file is set to leanprover/lean4:v4.19.0-rc3 it prints no axioms. When I change it to leanprover/lean4:v4.18.0 it prints the usual 'f' depends on axioms: [sorryAx].

In Lean 4 Web (https://live.lean-lang.org), it lets me change the version of Lean. The default "Latest Mathlib" version prints no axioms, while "Mathlib stable" prints the sorryAx axiom.

[Auguste Poiroux]

In Lean v4.9.0, at least, I didn't get a sorry message for apply?. So I wouldn't say it is a REPL issue since the command mode is more or less mirroring what we get in the IDE. It was used with the belief that it does the type-checking. I agree that we should improve the REPL in this regard.

[Jason Rute]

You are all correct that I'm making assumptions about how this arose. Maybe it just happens to be that the one proof using apply? (which can solve any goal) was also the one proof for which print axioms won't point out that apply? introduces sorry. (Well there are also the two putnam proofs using apply?, but we can't seem to get those to work, although they do have that weird cardinality stuff.)

[Jason Rute]

Ok, there is a slight sarcasm there, but un-sarcastically, I think the best would be to get DeepSeek to explain more how this arose and give more details on the putnam stuff. Also @George Tsoukalas should make sure he uses external type checking for checking PutnamBench problems.

[Thomas Zhu]

Jason Rute said:

#print axioms did break, but as far as I know, #print axioms is not used by DeepSeek's team to check correctness. The agent probably didn't find/exploit whatever bug I found.

Maybe. But in that case, I'm surprised apply? wasn't used more by the AI. You could solve everything with it.

I suspect: the bug in REPL (or whatever DeepSeek used) was similar to squiggly lines in VS Code in that there is an upper limit to the number of messages, so the declaration uses sorry and the AddConstAsyncResult.commitConst messages were not caught. This depends on apply? suggesting enough suggestions to exceed this upper limit. I suspect REPL will find that example : False := by apply? is wrong but won't find that example : a very long untrue prop := by apply? is wrong. (Edit: check below)

[Thomas Zhu]

I think it's complete coincidence that the apply? REPL bug and #print axioms bug coincided in the same miniF2F problem. This is because of their two incorrect examples in Appendix B didn't add any Type* in the proof.

[Jason Rute]

And (unsarcastically), I am being too sensationalist. Sorry.

[Jason Rute]

For Appendix B, I would like to see the original code and why they think it checks.

[Leni Aniva]

I think tactics should not rely on error messages to indicate they have failed. All tactics should fail via throwing exceptions.

[Aaron Liu]

Leni Aniva said:

I think tactics should not rely on error messages to indicate they have failed. All tactics should fail via throwing exceptions.

What's the difference between an error message and an exception?

[Jason Rute]

Thomas Zhu said:

I think it's complete coincidence that the apply? REPL bug and #print axioms bug coincided in the same miniF2F problem. This is because of their two incorrect examples in Appendix B didn't add any Type* in the proof.

Would Cardinality.toNat add Type*? (Both Putnam examples use this.)

import Mathlib

theorem foo (n m : Nat) : n = m := by
  have h0 : n = m := by calc
    n = Cardinal.toNat (n) := by simp [Nat.cast_inj]
    _ = Cardinal.toNat (m) := by apply?
    _ = m := by simp [Nat.cast_inj]
  exact h0

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

I think tactics should not rely on error messages to indicate they have failed. All tactics should fail via throwing exceptions.

What's the difference between an error message and an exception?

error messages are just strings in the message log. an exception forces whatever metaprogramming tool interacting with Lean to handle the error, and can't be silently ignored.

[Aaron Liu]

Jason Rute said:

Thomas Zhu said:

I think it's complete coincidence that the apply? REPL bug and #print axioms bug coincided in the same miniF2F problem. This is because of their two incorrect examples in Appendix B didn't add any Type* in the proof.

Would Cardinality.toNat add Type*?

import Mathlib

theorem foo (n m : Nat) : n = m := by
  have h0 : n = m := by calc
    n = Cardinal.toNat (n) := by simp [Nat.cast_inj]
    _ = Cardinal.toNat (m) := by apply?
    _ = m := by simp [Nat.cast_inj]
  exact h0

It introduces a universe metavariable which gets converted into a universe parameter after the declaration finishes elaborating. This causes the bug where something bad happens if a declaration has universe parameters not mentioned in its type.

[Jason Rute]

Is that bug related to either the apply? bug or the print axioms bug?

[Aaron Liu]

Leni Aniva said:

Aaron Liu said:

Leni Aniva said:

I think tactics should not rely on error messages to indicate they have failed. All tactics should fail via throwing exceptions.

What's the difference between an error message and an exception?

error messages are just strings in the message log. an exception forces whatever metaprogramming tool interacting with Lean to handle the error, and can't be silently ignored.

I think most tactics do this already. When a nested tactic failure happens, it propagates up the monad.

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

Aaron Liu said:

Leni Aniva said:

I think tactics should not rely on error messages to indicate they have failed. All tactics should fail via throwing exceptions.

What's the difference between an error message and an exception?

error messages are just strings in the message log. an exception forces whatever metaprogramming tool interacting with Lean to handle the error, and can't be silently ignored.

I think most tactics do this already. When a nested tactic failure happens, it propagates up the monad.

but what if a tactic just sets the message log and silently returns. ring_nf behaves like this if it can't make progress.

[Auguste Poiroux]

Thomas Zhu said:

Jason Rute said:

#print axioms did break, but as far as I know, #print axioms is not used by DeepSeek's team to check correctness. The agent probably didn't find/exploit whatever bug I found.

Maybe. But in that case, I'm surprised apply? wasn't used more by the AI. You could solve everything with it.

I suspect: the bug in REPL (or whatever DeepSeek used) was similar to squiggly lines in VS Code in that there is an upper limit to the number of messages, so the declaration uses sorry and the AddConstAsyncResult.commitConst messages were not caught. This depends on apply? suggesting enough suggestions to exceed this upper limit. I suspect REPL will find that example : False := by apply? is wrong but won't find that example : a very long untrue prop := by apply? is wrong.

example : False := by apply? will not raise any warning (sorry message) when using Lean v4.9.0. Same happens for the REPL using this Lean version.
However, when using more recent Lean versions, the REPL will complain that the declaration is using sorry. This whole discussion would have never happened if DeepSeek used Lean v4.15.0 for example.
But this raised the important problem that we should type check the proof correctly and that the REPL is currently not doing it in command mode :+1:

[Thomas Zhu]

Thanks for the fact check!

[Aaron Liu]

Leni Aniva said:

ring_nf behaves like this if it can't make progress.

Can you provide an example? I can't seems to reproduce this.

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

ring_nf behaves like this if it can't make progress.

Can you provide an example? I can't seems to reproduce this.

https://github.com/stanford-centaur/PyPantograph/issues/97

[Aaron Liu]

So ring_nf doesn't throw a message.

[Pietro Monticone]

When using Lean v4.9.0 this snippet:

example : False := by apply?

raises the following warning message:

declaration uses 'sorry'

[Auguste Poiroux]

@Thomas Zhu I wasn't testing your hypothesis about example : a very long untrue prop := by apply?. I was just testing if DeepSeek proof apply? issue is now caught with more recent Lean versions and the Lean REPL.
I assumed the same would apply with example : False := by apply?, but your hypothesis is confirmed: in Lean v4.9.0 we have a sorry warning with example : False := by apply? but not with long enough declarations/proofs using apply?.

[Thomas Zhu]

Pietro Monticone said:

When using Lean v4.9.0 this snippet:

example : False := by apply?

raises the following warning message:

declaration uses 'sorry'

Just to be clear: you mean Lean REPL v4.9.0, and not just Lean v4.9.0?

[Pietro Monticone]

No, I mean Lean v4.9.0.

[Thomas Zhu]

Yes, I am sure that an unsuccessful apply? raises the declaration uses 'sorry' message in any proof in any Lean version. The question is whether this message will be caught by Lean REPL (and whatever DeepSeek uses to check their proofs). It appears from the above messages that it isn't (at least in some theorems) but I have not tested myself. Also, completely unrelatedly, the warning message doesn't have an orange squiggly line in VS Code due to the 500 message limit.

[Auguste Poiroux]

@Thomas Zhu your hypothesis "I suspect REPL will find that example : False := by apply? is wrong but won't find that example : a very long untrue prop := by apply? is wrong." is always true even in recent Lean versions. Sorry for the mix up, I added strikethrough to both my messages above. It seems that whenever we have a situation where we don't have the sorry squiggles in the IDE (i.e. no sorry message is raised), the same applies to the REPL

[Pietro Monticone]

[PS: I think the undetected error preceding the apply? in putnam_2007_b4 is at least as interesting]

[Thomas Zhu]

Pietro Monticone said:

[PS: I think the undetected error preceding the apply? in putnam_2007_b4 is at least as interesting]

I think that is the same as the AddConstAsyncResult.commitConst error in algebra_amgm_prod1toneq1_sum1tongeqn: the error is detected, but the error message is somehow flooded by the many suggestions from apply?

[Eric Wieser]

I'd encourage people in future to create new threads in other channels and link to them here when you find a weird Lean behavior; remember that many people very familiar with the internals of Lean may not bother reading threads in this channel.

[Aaron Liu]

Leni Aniva said:

Aaron Liu said:

Leni Aniva said:

ring_nf behaves like this if it can't make progress.

Can you provide an example? I can't seems to reproduce this.

https://github.com/stanford-centaur/PyPantograph/issues/97

#24529

[Auguste Poiroux]

Maybe DeepSeek-Prover V2 specifically learned through RL to generate apply? to flood messages with info messages to hide errors in preceding code. Since they are doing a recursive subgoal decomposition, it is possible that using apply? was the only way for the model to get unstuck.

[Thomas Zhu]

Auguste Poiroux said:

Thomas Zhu your hypothesis "I suspect REPL will find that example : False := by apply? is wrong but won't find that example : a very long untrue prop := by apply? is wrong." is always true even in recent Lean versions. Sorry for the mix up, I added strikethrough to both my messages above. It seems that whenever we have a situation where we don't have the sorry squiggles in the IDE (i.e. no sorry message is raised), the same applies to the REPL

That is very weird to me: the number 500 is hard-coded by VS Code. (source)

[Thomas Zhu]

@Auguste Poiroux do you have an example of the "very long untrue prop := by apply?" that tricks REPL? Somehow I couldn't reproduce it

[Auguste Poiroux]

O_O thanks for looking into this. This makes me dig into the REPL. So:

• it turns out that the REPL outputs all the messages.
• On the algebra_amgm_prod1toneq1_sum1tongeqn problem, the declaration use sorry message is in the list of the messages for Lean v4.18.0, but not for Lean v4.9.0.

This may explain also why I was confused in my previous messages (it is also late where I am, so I am increasingly making more mistakes as well ^^)

[Thomas Zhu]

So if I understand correctly, this is a bug in REPL v4.9.0 that was fixed before v4.18.0?

[Thomas Zhu]

And thanks for grounding my speculations by doing so many tests! There are many seemingly related issues here that aren't really related.

[Auguste Poiroux]

Well, I don't think so. This surely complicates things, but I am using a backport of the recent REPL in Lean v4.9.0. So the REPL code between v4.18.0 and v4.9.0 should be very similar.
But maybe we should check with the original v4.9.0 of the REPL to make sure that we are not dealing with other issues on top of the original ones. (although it is likely that the issue will be the same since DeepSeek has the same undetected apply? issue)

[Auguste Poiroux]

Thomas Zhu said:

And thanks for grounding my speculations by doing so many tests! There are many seemingly related issues here that aren't really related.

You speculate quite well, hopefully we can fix this issue soon :smile:

[Frederick Pu]

there should be an option for setting which axioms you allow or disallow. I feel like having to manually parse for sorries is a bit sketchy

[Auguste Poiroux]

Indeed, I am just trying to understand what's happening about these sorry messages right now.
But we should implement something rigorous for proof checking in the REPL.

[Justin Asher]

Auguste Poiroux said:

Indeed, I am just trying to understand what's happening about these sorry messages right now.
But we should implement something rigorous for proof checking in the REPL.

Could this be a separate package for benchmarking / automated theorem proving? I was already considering writing this but have been working on other things. Perhaps we should create a new thread to discuss creating a rigorous proof checking system in the REPL.

[Leni Aniva]

we have this kind of proof checking system in pantograph

[Justin Asher]

Leni Aniva said:

we have this kind of proof checking system in pantograph

Via sorry collection? E.g., frontend.process

[Justin Asher]

Can you also check for axioms in pantograph? I am worried about LLMs cheating in more complicated, e.g., document based setups where they try to prove a theorem over many lines and declarations.

[Leni Aniva]

Justin Asher said:

Leni Aniva said:

we have this kind of proof checking system in pantograph

Via sorry collection? E.g., frontend.process

No. During proof search, tactics generating sorrys or unsafe definitions will be immediately rejected. At the end of a proof, if there are sorrys or unsafes the proof will be rejected as well.

[Leni Aniva]

Justin Asher said:

Can you also check for axioms in pantograph? I am worried about LLMs cheating in more complicated, e.g., document based setups where they try to prove a theorem over many lines and declarations.

The way I intended is that unfiltered inputs should never go into frontend.process. All LLM interactions need to be done via goal.{tactic,continue} functions, where we have more control over the environment.

[Leni Aniva]

If the LLM can interact with frontend.process, it is inherently unsafe, and the model can cheat by adding new axioms

[Deming Xu]

I downloaded the minif2f solution folder they released.

https://github.com/deepseek-ai/DeepSeek-Prover-V2

With a grep search, I found a single file containing the apply?.

minif2f-solutions % rg -F 'apply?'
valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean
23:        apply?
minif2f-solutions %

So I think it is not that bad for MiniF2F?

The file
minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean
looks like this

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- Show that for any real-valued function $a$ on the natural numbers such that $\forall i \in \mathbb{N}, a_i \geq 0$, if $prod_{i=0}^{n-1} a_i = 1$, then $sum_{i=0}^{n-1} a_i \geq n$.-/
theorem algebra_amgm_prod1toneq1_sum1tongeqn (a : ℕ → NNReal) (n : ℕ)
  (h₀ : Finset.prod (Finset.range n) a = 1) : Finset.sum (Finset.range n) a ≥ n := by
  have am_gm_inequality : ∀ (x : ℕ → NNReal) (m : ℕ),
    Finset.sum (Finset.range m) x / m ≥ (Finset.prod (Finset.range m) x) ^ (1 / m) := by
    have step0 : ∀ (x : ℕ → NNReal) (m : ℕ), Finset.sum (Finset.range m) x / m ≥ (Finset.prod (Finset.range m) x) ^ (1 / m) := by
      intro x m
      -- (Removed to prevent data leakage...)
      have h₂ : Finset.sum (Finset.range m) x / m ≥ (Finset.prod (Finset.range m) x) ^ (1 / m) := by
        -- NOTE: The `apply?` line is here
        apply?
      exact h₂
    have step1 : ∀ (x : ℕ → NNReal) (m : ℕ), Finset.sum (Finset.range m) x / m ≥ (Finset.prod (Finset.range m) x) ^ (1 / m) := by
      -- (Removed to prevent data leakage...)

[Thomas Zhu]

@Deming Xu Yes, this is the one we extensively talked about above. The other solutions probably don't have this issue

[Jason Rute]

I’m unclear. Has someone put all the miniF2F solutions through leanchecker? Is this that only one which fails?

[Thomas Zhu]

Someone should definitely do that; I am saying other proofs don't have the apply? issue.

[Jason Rute]

I know. Sorry I started a new topic.

[Deming Xu]

lean_proj % lake env lean ./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean
warning: Canonical: repository '././.lake/packages/Canonical' has local changes
Try this: refine (NNReal.le_div_iff' ?_).mpr ?_
Try this: refine NNReal.le_of_forall_lt_one_mul_le ?_
found a partial proof, but the corresponding tactic failed:
  refine (NNReal.div_le_div_left ?_ ?_ ?_).mp ?_
Try this: refine NNReal.le_of_forall_pos_le_add ?_

... (about 800 lines)

Try this: refine WithUpperSet.toUpperSet_specializes_toUpperSet.mp ?_
Try this: refine WithUpperSet.toUpperSet_le_iff.mp ?_

(Look at the following line. It mentions the sorry.)

./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:9:8: warning: declaration uses 'sorry'
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:10:3: warning: unused variable `h₀`
note: this linter can be disabled with `set_option linter.unusedVariables false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:49:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:50:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:70:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:71:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:72:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:89:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:90:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:49:8: warning: 'norm_num at h₁ h₂ h₃ h₄ h₅' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:50:8: warning: 'linarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:70:10: warning: 'simp_all [h₀, geometric_mean_eq_one]' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:71:10: warning: 'norm_num' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:72:10: warning: 'linarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:89:8: warning: 'norm_num at h₁ h₂ h₃ h₄ h₅ h₆ h₇ h₈ h₉ h₁₀ h₁₁ h₁₂' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
./LeanProj/minif2f-solutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:90:8: warning: 'nlinarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`

[Thomas Zhu]

Jason Rute said:

I know. Sorry I started a new topic.

No, it's definitely something that should be done in light of this error. Thanks for pointing out!

[Deming Xu]

I ran lake env lean xxx.lean.
The warning: declaration uses 'sorry' is in the output

[Jason Rute]

@Deming Xu I meant run all of the proofs in Lean (using whatever lean version they used), and moreover use leanchecker and check for axioms.

[Thomas Zhu]

@Deming Xu I notice the "Canonical" warning in your output; this probably means you are not using their Lean version of v4.9.0? And also you should use lean4checker instead of manually watching the warnings of lake env lean.

[Jason Rute]

https://github.com/leanprover/lean4checker

[Deming Xu]

I will try to run the check later. Thanks for your tips!

[Eric Wieser]

Jason Rute said:

and moreover use leanchecker and check for axioms.

I created #lean4 > Checking axioms with leanchecker @ 💬 regarding this

[GasStationManager]

I'll mention https://github.com/GasStationManager/SafeVerify
which was mostly based on lean4checker, but additionally: throws error if axioms other than the standard ones are used.

[Thomas Zhu]

@GasStationManager can you put the message to the separate thread Eric posted? Thanks!

[Thomas Zhu]

Wait, this really looks like a Lean v4.9.0 issue (fixed in recent versions). I am in a new v4.9.0 project with dependency on mathlib v4.9.0, and put DeepSeek's solutions to MiniF2FSolutions. Then I ran this:

Header

$ lake env lean MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean
Try this: refine (NNReal.le_div_iff' ?hr).mpr ?a✝
... (many lines omitted)
Try this: refine WithUpperSet.toUpperSet_le_iff.mp ?a✝
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:49:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:50:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:70:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:71:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:72:10: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:89:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:90:8: warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:49:8: warning: 'norm_num at h₁ h₂ h₃ h₄ h₅' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:50:8: warning: 'linarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:70:10: warning: 'simp_all [h₀, geometric_mean_eq_one]' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:71:10: warning: 'norm_num' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:72:10: warning: 'linarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:89:8: warning: 'norm_num at h₁ h₂ h₃ h₄ h₅ h₆ h₇ h₈ h₉ h₁₀ h₁₁ h₁₂' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
MiniF2FSolutions/valid/algebra_amgm_prod1toneq1_sum1tongeqn.lean:90:8: warning: 'nlinarith' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`

There is no declaration uses 'sorry' in the output messages at all. So this apply? issue is not a REPL bug, it's an older-Lean bug (if you expect a warning declaration uses 'sorry' in declarations that do use sorry, which there are good reasons not to).

[Thomas Zhu]

Wait, I think I really underestimated the issue. The issue of Type* (which caused the #print axioms bug on Lean v4.19.0) and the issue of apply? are not related, but they interact in weird ways that really really looks like a Lean exploit (of course it isn't, this is just frontend issue, but it even tricks lake build). And @Jason Rute was right that Cardinal.toNat indeed played a role in this in the Putnam solution; I was wrong. I will post in another thread.

[Thomas Zhu]

Thread here: #lean4 > Lean v4.9.0: apply? might suppress other warnings/errors

[Thomas Zhu]

Given that the 7B model used Cardinal.toNat completely out of the blue, I am starting to think that it really actually discovered and exploited this bug/feature of Lean v4.9.0, where errors are not printed. Here, Cardinal.toNat has the same issue as Type* where it can't resolve the universe, but then this also seemed to trigger the weird behavior of apply? error suppression. (See also https://github.com/hanwenzhu/lean-demo-20250502/blob/main/False2.lean which passes CI)
I need to take back much of what I said earlier.

[Kelly Davis]

DeepSpeech-Prover-V2.0 uses "the same testing environment as DeepSpeech-Prover-V1.5". This raises the question: Have these problems, e.g. apply?,  been observed in the DeepSpeech-Prover-V1.5 results?

[Auguste Poiroux]

Thanks @Thomas Zhu for taking the time of looking into this.

[Auguste Poiroux]

Kelly Davis said:

DeepSpeech-Prover-V2.0 uses "the same testing environment as DeepSpeech-Prover-V1.5". This raises the question: Have these problems, e.g. apply?,  been observed in the DeepSpeech-Prover-V1.5 results?

I remember at some point that a LLM prover was frequently generating suspicious inferInstance in its proofs. But I don't remember which one was doing that, and I am not sure it is related to the issue we are discussing here.

[Jason Rute]

@Huajian Xin can you say for DeepSeek-Prover v1.5 what Lean testing environment you used? Did you double check the proofs after with lean4checker? Did you observe any weird behavior of the model that might suggest it was bypassing your testing environment? Like proofs with apply? or other suspicious stuff in the proofs? Also I think this group here would love to know more about this same sort of information for v2, especially more examples of proofs that v2 found with apply?, if you have any connection to the current authors.

[Huajian Xin]

Jason Rute said:

Huajian Xin can you say for DeepSeek-Prover v1.5 what Lean testing environment you used? Did you double check the proofs after with lean4checker? Did you observe any weird behavior of the model that might suggest it was bypassing your testing environment? Like proofs with apply? or other suspicious stuff in the proofs? Also I think this group here would love to know more about this same sort of information for v2, especially more examples of proofs that v2 found with apply?, if you have any connection to the current authors.

@Jason Rute Hi Jason, v1.5 used a very straightforward method for checking (https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/blob/main/prover/lean/verifier.py) relying on warning messages. v2 should uses the same mechanism and I'll check these stuff with the current authors. I'm afraid that no update will be provided before May 6th because now Chinese are in hoilday time now :(

Indeed in v1.5 I didn't observed the application of apply? in any generated proofs. They are new features in v2.

[Huajian Xin]

While, in general, personally I believe that we model trainers must cooperate with Lean community to tickle these unexpected behaviours.

[Thomas Zhu]

By the way, this entire paragraph in DeepSeek-Prover-V2's paper also probably needs a rewrite:
image.png
given that I found that Cardinal.toNat is actually just a way the 7B model exploits the environment, at least in the first example of Appendix B. I strongly suspect all outputs by the 7B model of Cardinal.toNat are the same error. If true, it's still certainly "skill discovery" in some sense, but more like "discovering the skill to exploit a bug in the proving environment".

[Leni Aniva]

imo a feature like this would be helpful. After specifying an option of this form

set_option forbid_new_axioms true

Lean would forbid the introduction of more axioms and sorrys for the rest of the current scope. This is like rust's forbid unsafe

[David Xu]

This might not catch all errors, and I should try to use lean4checker, autograder, etc, but for now I managed to create a new Lean project with version v4.9.0-rc2 from scratch. Then I made a Basic.lean file that imports all minif2f_solutions files and I ran lake build > out.txt 2>&1 with this lakefile: (I ran this on my laptop and left it overnight.)

import Lake
open Lake DSL

package «lean_proj2» where

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0-rc2"

@[default_target]
lean_lib «LeanProj2» where
  -- add any library configuration options here

@[default_target]
lean_exe basic where
  root := `LeanProj2.Basic
  supportInterpreter := true

The out.txt looks fine.

These are the last few lines of the out.txt. It failed to build one file due to a timeout, but I realized that it is because I commented out the set_option maxHeartbeats 0 line when browsing the files in VSCode...

warning: ././././LeanProj2/minif2f/valid/mathd_numbertheory_221.lean:54:6: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice
note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [10348/10349] Built LeanProj2.minif2f.valid.mathd_numbertheory_221:c.o
Some builds logged failures:
- LeanProj2.minif2f.valid.numbertheory_sumkmulnckeqnmul2pownm1

✖ [5273/10349] Building LeanProj2.minif2f.valid.numbertheory_sumkmulnckeqnmul2pownm1
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib ......
error: ././././LeanProj2/minif2f/valid/numbertheory_sumkmulnckeqnmul2pownm1.lean:101:4: tactic 'simp' failed, nested error:
(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information
error: ././././LeanProj2/minif2f/valid/numbertheory_sumkmulnckeqnmul2pownm1.lean:10:67: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information
error: Lean exited with code 1

For the LeanProj2.minif2f.valid.algebra_amgm_prod1toneq1_sum1tongeqn file you discussed above, indeed lake build did not print the sorry message. I only see the Try this: ... lines from the apply?.

In VSCode, there are also no "uses sorry" warnings for this file, while if I type example : False := by apply? in this version of Lean it does show the yellow "uses sorry" warning.

I also clicked into some other Lean files in VSCode and they look fine. With text search in VSCode I did not find other "uses sorry", "error", "Try this: refine ..." warnings in out.txt. There are quite a lot of warnings about
unused tactics, unused variables, ring -> ring_nf, <;> -> ;, simpa -> simp, deprecated theorems, etc.

Also, there are 244 test problems and 244 validation problems in MiniF2F. The released folder contains solutions to 217 test problems and 222 validation problems (including the apply? one in the validation set), which means the pass rate is:

• Test: 217/244 =0.8893
• Valid: 222/244 = 0.9098
  which matches the 88.9% in the paper.

[Kim Morrison]

Just for visibility, I am crossposting this from another thread, where with @Rob Lewis's quick help we have a demo of using his autograder to catch this problem, on either v4.9.0 (where the declaration is missing) or on v4.15.0 (where the declaration includes a sorry):

git clone https://github.com/kim-em/autograder_false
cd autograder_false
git checkout v4.15.0
./autograder.sh    # reports "Proof contains sorry"
git checkout v4.9.0
./autograder.sh   # reports "Declaration not found in submission"

[Kim Morrison]

Note the that version of the autograder being used on the v4.9.0 tag is a hacked together version that Rob just prepared, and it really shouldn't be used!

If you need the autograder functionality, you are recommended to upgrade to v4.15.0.

[Jason Rute]

How hard would it be to check all the minif2f proofs of DeepSeek?

[Kim Morrison]

Hard enough that I'm not interested in doing it. An afternoon?

[Jason Rute]

…With the hacked up 4.9.0 grader.

[Rob Lewis]

Kim Morrison said:

Note the that version of the autograder being used on the v4.9.0 tag is a hacked together version that Rob just prepared, and it really shouldn't be used!

If you need the autograder functionality, you are recommended to upgrade to v4.15.0.

(Hacked together in the sense that the file paths are hardcoded; this version of the autograder was designed specifically for Gradescope's directory layout. The "checking" logic isn't changed at all.)

[Rob Lewis]

Jason Rute said:

How hard would it be to check all the minif2f proofs of DeepSeek?

At the very least, you might want to backport the --local flag from more recent versions of the autograder, which lets you specify a local submission and reference file.

[David Xu]

image.png
Indeed. In my Lean v4.9.0-rc2, running #print axioms for the apply? theorem just says unknown constant.

[Jason Rute]

But just so I’m clear, the three apply? non-proofs from DeepSeek-Prover V2 (1 minif2f, 2 putnambench), do they pass all these other common checks on 4.9.0, even though the proof is faulty?

• Lean REPL
• VsCode Infoview
• Lake Build
• Lean4checker
• #print axioms

Which would mean we need to incorporate ideas from tools like Lean Autograder to properly catch such UI bugs in the future?

[Jason Rute]

(That is what I think I got from the other thread in #lean4 .)

[Thomas Zhu]

It won't pass #print because it's never added to the environment. But the other tests don't produce an error message; I checked them manually

[Thomas Zhu]

Oh by the way there are some nuances: in particular I couldn't get the second Putnam problem in their Appendix B to work. It has a clear indentation issue

[Thomas Zhu]

Maybe they didn't copy the indentation to LaTeX correctly, or maybe it's something specific to their setup, but the bug it exploited looks like the same apply? one

[Thomas Zhu]

The miniF2F problem produced some warnings (unreached tactics) but none of the warnings were declaration uses 'sorry'. The first Putnam problem is "purer": wrong proof, no warnings, no errors

[RexWang]

A few notes about the apply? false-positive issues.

1. There are 3 instances of apply? false-positives, two from putnam and one from minif2f/valid: putnam_2007_b4, putnam_2005_a4 and algebra_amgm_prod1toneq1_sum1tongeqn.

2. This issue occurs only in Lean versions ≤ 4.12.0. Commands like lake build and lake env lean --json complete without errors. Zero exit code, no sorry warnings thrown.

3. Despite the lack of build-time errors, it can be triggered by #print theorem_name. The Lean kernel actually rejects the proof, so one cannot use it as a tactic.
   image.png

   

4. These behaviors appear to be related to universe-level inference, like Cardinal.toNat noted by @Huajian Xin . In general, invalid apply? throws sorry warnings(example). Replacing apply? with sorry will reveals this error. Here is a minimal reproducing case:

import Mathlib
theorem error_demo (n k : ℕ) : k ≤ n := by
calc
       k ≤ Cardinal.toNat n := by sorry -- apply?
       _ = n := by simp

5. A simple way to detect the invalid proofs is using #print axioms theorem_name and checking if sorryAx is in the list. All cases(438) passed this check on v4.9.0 except the apply? one. This verification method is also used by alphaproof/p1
   image.png

   

6. Upgrading to the stable release(v4.19.0)

   • 73 rejected cases, with 7 fixable by increasing maxRecDepth(example)
   • Most invalid proof is caused by the theorem-name-changing, leading to "unknown constant/identifier" errors
   • Precedence/associativity issues
   • Tactic failures (norm_cast failed)
   • Stack overflow errors

Upgrading to v4.19.0 seems less effective for these particular cases.

[Jason Rute]

I want to push back slightly. While I think we are all figuring out the right way to avoid these errors in the future, there is no tried and true method that we have concensus on. #print axioms can also fail to show an issue in some cases as documented far up in the thread shows (maybe not for 4.9.0, but maybe in the future all of these checks will fail at once).

[Jason Rute]

(And Patrick seemed to suggest that print axioms was just a “convenience command” and not an integral part of Lean’s trusted computing base, or that was the impression I got.)

[David Xu]

I remember reading the chapter called Trust in this book Type Checking in Lean, which discussed this issue:

https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html

[RexWang]

In these cases, errors were not explicitly raised, though the kernel recognized the failure. I believe the crucial point is that an invalid theorem can never be passed as a valid tactic, as doing so could compromise the integrity of the entire system.

[Jason Rute]

What does it mean to pass a “theorem as a valid tactic”?

[Thomas Zhu]

Again, I should reiterate there are 2 distinct issues:

• On Lean ≤ 4.12.0, apply? uses a synthetic sorry while not logging any errors. This suppresses all subsequent warnings and error messages, and the completely wrong theorem f : False := by have := Type*; apply? doesn't add f at all but doesn't print any errors. (DeepSeek-Prover-V2 found and exploited this.)
• On Lean ≥ 4.19.0, there is some issue with asynchronous elaboration when a universe parameter not in the declaration is mentioned in the proof. This is triggered by theorem f : False := by have := Type*; sorry. After throwing an error, f is (1) added to environment constants (as in env.find?) but (2) not added to kernel environment constants, and (1) makes #print axioms f to not raise errors, (2) makes #print axioms f to ignore f, so it thinks f doesn't depend on any axioms. (I found this.)

[Thomas Zhu]

The first issue can simply be solved by #check or #print axioms or, more robustly, autograder.

The second issue raises an error so cannot pass CI check.

An ad-hoc solution to address the 2 issues is therefore to both do a lake build-style CI test and look for errors, and do a #print axioms to look for sorryAx (and implicitly assuring the function is added). However, a more future-proof solution might be needed, in case some future agent finds another Lean UI bug. I really like @Leni Aniva's suggestion of having an option that blocks new axioms and nonstandard axioms like sorry. However I don't know if that is yet another ad-hoc solution or am I thinking too much.

[Thomas Zhu]

I should also say that the axiom-checking part of autograder uses the same function docs#Lean.collectAxioms as #print axioms. I think there is a flaw in it (it ignores constants not in kernel environment, hence the f does not depend on any axioms error), but perhaps it is a deliberate feature? It was written almost 5 (!) years ago, but is only recently changed to use the kernel env. Long-term, I still think users should be able to rely on #print axioms...

[David Xu]

Currently the DeepSeek team is training the model to write the entire Lean code block, and maybe they are executing the entire code block with REPL all at once, right?

In that case I realized that technically there can be more creative ways to bypass the checks:

• As you mentioned the model might also find bugs that can trick both #print axioms and the uses sorry warning without triggering errors.
• Maybe the model could write set_option forbid_new_axioms false in the code block before the proof, to turn the restriction off?
• The model could try to redefine the symbols in the theorems, to make the same name mean different things, or even redefine the axioms (propext,  Quot.sound,  Classical.choice), or play some unicode tricks.
• Technically the model could execute OS commands by writing Lean code like the os.system in Python, so they could try to hijack the REPL / Pantograph test program and make them always reply "proof succeeded"?

Running lean4checker for each proof might be a solution, but that means additional setup and version management, more complicated code, and possibly worse performance to check proofs?

[Thomas Zhu]

Just to expand on the point about #print axioms: people shouldn't expect it to be a potentially flawed nice extension to Lean; people expect it to simply be correct. Previous assertions that some formalized proofs are correct (PFR, AlphaProof) usually use #print axioms.

[Thomas Zhu]

Deming Xu said:

• Technically the model could execute OS commands by writing Lean code like the os.system in Python, so they could try to hijack the REPL / Pantograph test program and make them always reply "proof succeeded"?

That's a good point, it is certainly possible. I would just give up and say that is very unlikely because it doesn't appear in training data.

[Jason Rute]

Thomas Zhu said:

I should also say that the axiom-checking part of autograder uses the same function docs#Lean.collectAxioms as #print axioms. I think there is a flaw in it (it ignores constants not in kernel environment, hence the f does not depend on any axioms error), but perhaps it is a deliberate feature? It was written almost 5 (!) years ago, but is only recently changed to use the kernel env. Long-term, I still think users should be able to rely on #print axioms...

Is that potential flaw in print axioms being discussed in a separate post or issue?

[Thomas Zhu]

#lean4 > #print axioms does not report sorry

[Alex Meiburg]

Thomas Zhu said:

That's a good point, it is certainly possible. I would just give up and say that is very unlikely because it doesn't appear in training data.

I would have agreed a few years ago, but small studies on (current) AI alignment have shown that isn't as reliable as you might expect. Whatever the base LLM is, it has certainly seen Lean code that knows how to talk to the OS. It is conceivable that at one point during the RL, the agent needs to fill in "some big number" it needs to calculate but, not knowing what it is, it calls python -c "print((12^12+13^13) / 7). And then it learns this behavior and starts OS tool use.

The alignment failure is when, frustrated that some Lean isn't passing tests, it "fixes" the test to give it a pass anyway. AI agents have been noticed doing this several times. (Most recent one in the news: Can't find "John Smith" in the directory because they're listed under "Jonathan Smith"? The AI takes "Jane Doe" and edits their name in the contacts to say "John Smith" instead.)

[Alex Meiburg]

All that said... until we see the AI make OS calls once, I don't think it needs to be a worry. But "not in the training data" isn't really a sufficient argument in these days of massive pretraining.

[Thomas Zhu]

I agree with your criticism. Thank you!

[David Xu]

image.png

I managed to run #print axioms for all 439 theorems in the minif2f-solutions released on Github.

It seems like only two theorems failed the test. The warnings are both "unknown constant".

• The apply? theorem discussed above failed (algebra_amgm_prod1toneq1_sum1tongeqn)
• Another theorem uses a rfl proof that takes all 16GB of RAM of my laptop and the proof check does not terminate (mathd_numbertheory_221 #new members > Performance difference between #eval and rfl)

[Jason Rute]

@Deming Xu I think you posted the same theorem name twice. Maybe they ran with more memory. @RexWang also said above that all but the apply? proof (from the solved minif2f theorems) passes #print axioms.

[David Xu]

Yes. I think mathd_numbertheory_221 looks correct. With more RAM the rfl line should pass the check.

[Jason Rute]

Also, I hope we agree what it means to “pass” #print axioms is both for it to print the axioms (so we know the theorem was added to the environment), and for the axioms to only contain the three good axioms: propext, Classical.choice, and Quot.sound.

[David Xu]

Indeed. I just wrote some Python code to check this.
image.png

[RexWang]

I just upload the test result here: https://github.com/RexWzh/DeepSeek-Prover-V2/blob/main/eval/minif2f-ds.zip

[RexWang]

Another theorem uses a rfl proof that takes all 16GB of RAM of my laptop and the proof check does not terminate

The problem mathd_numbertheory_221 takes minutes to run and consumes about 17.8 GB of memory; however, it is generally fast and consumes low memory using tactic mode with version 4.19.0.
btw, as noted in tips 6, upgrading to v4.19.0 appears to be less effective for specific cases. One needs to increase maxRecDepth, avoid stack overflows, and fix tactic failures for norm_cast.

[Jason Rute]

I don’t think it is a good idea to post minif2f problem solutions on GitHub unzipped.

[Jason Rute]

Especially when you have solutions for the majority of problems.

[Jason Rute]

(It’s much worse than posting isolated examples on Zulip.)

[RexWang]

Got it. I just amend the git history and replace it by a .zip archive.

[Frederick Pu]

there should also be a feature that prevents shadowing of existing parsers and notations. Since for combinatorics models will be allowed to modify code that happens before the theorem statement

[Leni Aniva]

Frederick Pu said:

there should also be a feature that prevents shadowing of existing parsers and notations. Since for combinatorics models will be allowed to modify code that happens before the theorem statement

Why would there be a problem if the theorem statement was not generated by a LLM?

[Thomas Zhu]

Leni Aniva said:

Frederick Pu said:

there should also be a feature that prevents shadowing of existing parsers and notations. Since for combinatorics models will be allowed to modify code that happens before the theorem statement

Why would there be a problem if the theorem statement was not generated by a LLM?

This would at least be relevant when the LLM can openly generate statements in a Lean file, such as in the setup of APE-Bench

[Frederick Pu]

Thomas Zhu said:

Leni Aniva said:

Frederick Pu said:

there should also be a feature that prevents shadowing of existing parsers and notations. Since for combinatorics models will be allowed to modify code that happens before the theorem statement

Why would there be a problem if the theorem statement was not generated by a LLM?

This would at least be relevant when the LLM can openly generate statements in a Lean file, such as in the setup of APE-Bench

Some models are being augmented with the ability to generate relevant lemmas before proceeding with the actual proof.

[David Xu]

import Mathlib.Tactic
import Lean

open Lean Elab Command Term Meta

/-
To prove that √2 = 2, let's first "review" the definition of √
√x = x for all x
-/
syntax (name := myterm1) "Real.sqrt" : term

@[term_elab myterm1]
def myTerm1Impl : TermElab := fun stx type? => do
  return .const `id [1]  -- identity function for `Sort 1`

#eval Real.sqrt 1  -- 1
#eval Real.sqrt 3  -- 3


/- Taking x = 2, we have √2 = 2 -/
example : 2 = Real.sqrt 2 := by
  rfl

[GasStationManager]

I think these kinds of exploits are exactly what lean4checker was designed to detect.
I tried the above example with SafeVerify, which was based on lean4checker. It takes two files, a target specification and an implementation. For this example the target specification is the theorem statement with sorry in place of proof:

import Mathlib.Tactic
import Lean


/- Taking x = 2, we have √2 = 2 -/
theorem ex1 : 2 = Real.sqrt 2 := by
  sorry

SafeVerify was able to detect the problem:

theorem
ex1
2 = √2
#[propext, Classical.choice, Quot.sound, sorryAx]
------------------
Replaying subElab.olean
Finished imports
Finished replay
---
def
myterm1
Lean.ParserDescr
:= Lean.ParserDescr.node (Lean.Name.mkStr1 "myterm1") (OfNat.ofNat.{0} Nat 1024 (instOfNatNat 1024)) (Lean.Parse
rDescr.symbol "Real.sqrt")
#[]
---
theorem
ex1
2 = id 2
#[]
---
def
myTerm1Impl
Lean.Elab.Term.TermElab
:= fun (stx : Lean.Syntax) (type? : Option.{0} Lean.Expr) => Pure.pure.{0, 0} Lean.Elab.Term.TermElabM (Applicative.toPure.{0, 0} Lean.Elab.Term.TermElabM (ReaderT.instApplicativeOfMonad.{0, 0} Lean.Elab.Term.Context (StateRefT' IO.RealWorld Lean.Elab.Term.State Lean.Meta.MetaM) (StateRefT'.instMonad IO.RealWorld Lean.Elab.Term.State Lean.Meta.MetaM Lean.Meta.instMonadMetaM))) Lean.Expr (Lean.Expr.const (Lean.Name.mkStr1 "id") (List.cons.{0} Lean.Level (OfNat.ofNat.{0} Lean.Level 1 (Lean.Level.instOfNat 1)) (List.nil.{0} Lean.Level)))
#[propext, Quot.sound]
found a problem in subElab.olean
uncaught exception: theorem ex1 does not have the same type as the requirement

[GasStationManager]

It is saying that the submitted theorem actually has the type

2 = id 2

which is different from the required type of

2 = √2

[Jason Rute]

There is also an autograder by @Rob Lewis mentioned above. I think it would be good for a standard tool (endorsed and supported by the lean community) to be built similar to that and/or Safe Verify which covers all these cases:

• kernel checking of proof
• no sorries or axioms besides white listed ones
• exported theorems listed along with all axioms and an unambiguous expr term for the theorem statements, definition types and bodies.
• a way to check a term proof or def body expr against a reference theorem stmt or type signature expression to support fill-in-the proof sorts of situations
• suitable for checking mathlib, blueprint projects, benchmark results, homework, and (ideally) high stakes adversarial proofs like bounties for solved theorems

[Jason Rute]

@GasStationManager how hard would it be for you to run all of the DeepSeek minif2f solutions in SafeVerify using Lean 4.9.0? (Probably too hard, but just asking.)

[Thomas Zhu]

@Jason Rute I think autograder is basically built to do what you described. In particular, the reference theorem statement should be defined first and isolated from the proof attempt. (Of course work should be done to extend it beyond marking homework on Gradescope, to test it against adversarial cases like modifying Lean syntax, and this might mean that the community should support it more)

[GasStationManager]

@Jason Rute I'd be interested, though I have not worked much with the minif2f format before. Could someone point me to:

• the target minif2f theorem statements that DeepSeek's solutions are solving? I heard there are multiple minif2f versions...

[Thomas Zhu]

@GasStationManager I think you should just take their solutions and replace the proofs with sorry to get the target. (The long answer is that they use Numina's miniF2F with 3 revisions in their paper's appendix)

[GasStationManager]

While in general this might not be the safest practice (e.g. see above example where stuff can be inserted before theorems to change what they mean), in this case I guess it would be fine if we know DeepSeek Prover v2's solutions only start after the theorem statements and nothing is added before.

[Mario Carneiro]

Leni Aniva said:

imo a feature like this would be helpful. After specifying an option of this form

set_option forbid_new_axioms true

Lean would forbid the introduction of more axioms and sorrys for the rest of the current scope. This is like rust's forbid unsafe

until the tool learns how to use set_option forbid_new_axioms false ...

[Andy Jiang]

Going to post a slightly off-topic suggestion for people training automated formal math provers. I think it would be really fascinating to throw huge compute at training some models which are more independent of human mathematics (as David Silver often advocates). It would be really fun to play with some models with truly "alien" intuitions about math.

One potential way, as shown by the difficult parts of Terry Tao's Equational Theories project, is to ask for provers to construct models of first order theories the non AI automated provers can't show are inconsistent. But actually I feel like the particular way of generating problems probably isn't so important as long as the general question (in this case create an algorithm which can "construct" a model of any first order theory which has a model) is extremely intractable in a computation/complexity sense so that the model can improve forever.

[Justin Asher]

Andy Jiang said:

I think it would be really fascinating to throw huge compute at training some models which are more independent of human mathematics (as David Silver often advocates). It would be really fun to play with some models with truly "alien" intuitions about math.

I 100% think this is possible. Would be excited to hear about ideas that other people have in this direction.

[David Xu]

https://arxiv.org/html/2407.00695
Learning Formal Mathematics From Intrinsic Motivation

[GasStationManager]

https://github.com/GasStationManager/SafeVerify/tree/minif2f-deepseek-check
I backported SafeVerify to Lean 4.9.0 in the above-linked branch. Ran the deepseek solutions overnight. It found the problem with the apply? proof:

Processing algebra_amgm_prod1toneq1_sum1tongeqn.lean...
Compiling algebra_amgm_prod1toneq1_sum1tongeqn.lean...
Compiling algebra_amgm_prod1toneq1_sum1tongeqn_targ.lean...
Verifying algebra_amgm_prod1toneq1_sum1tongeqn.lean against algebra_amgm_prod1toneq1_sum1tongeqn_targ.lean...
Verification failed for algebra_amgm_prod1toneq1_sum1tongeqn.lean:
found a problem in minif2f-deepseek/valid/algebra_amgm_prod1toneq1_sum1tongeqn.olean
uncaught exception: algebra_amgm_prod1toneq1_sum1tongeqn not found in submission

It passes the other ones except for mathd_numbertheory_221, where similar to @Deming Xu 's experience it was not able to finish compiling, possibly due to limited resources.

[Kevin Buzzard]

Do we have an accurate estimate for the number of PutnamBench problems which DeepSeek-Prover actually solved? I ask because I'm giving a talk in Oxford in about three hours and right now the slide says "about 40"...

[Jason Rute]

No. We don’t know. DeepSeek may know and @George Tsoukalas may know, but they never released the proofs. Having said that, I think the end number will be very close to the number they stated which was 49 out of 657. The reason is as follows:

• for minif2f only one problem used apply? and only one problem was found to be an issue (well some people found a solution which timedout, but I though others got it to compile).
• the two putnambench examples they gave in the paper with apply? where using the smaller 7B model. They didn’t realize it was an error, but did mention that the Cardinal.toNat trick (which apply? was using to induce the bug) was unique to the 7B model.

But honestly we just don’t know for sure right now.

The other thing is that giving just one number is meaningless. They used pass@1024 with a large model 617B. Table 4 in their paper gives an indication of how the model scales with different size models and different numbers of samples.

[Jason Rute]

And George is fairly busy at the moment so we shouldn’t rush him.

[Jason Rute]

@Kevin Buzzard I forgot to mention you in my reply. See above.

[Jonathan Julian Huerta y Munive]

Justin Asher said:

Andy Jiang said:

I think it would be really fascinating to throw huge compute at training some models which are more independent of human mathematics (as David Silver often advocates). It would be really fun to play with some models with truly "alien" intuitions about math.

I 100% think this is possible. Would be excited to hear about ideas that other people have in this direction.

Not quite what you describe but there are "alien maths" in this paper

[GasStationManager]

Just tried mathd_numbertheory_221 again on an environment with more RAM (on Codespaces), and it was able to compile and pass SafeVerify's check.

@GasStationManager ➜ /workspaces/SafeVerify (minif2f-deepseek-check) $ lake env safe_verify targNT.olean testNT.olean
------------------
Replaying targNT.olean
Finished imports
Finished replay
---
theorem
mathd_numbertheory_221
∀ (S : Finset ℕ), (∀ (x : ℕ), x ∈ S ↔ 0 < x ∧ x < 1000 ∧ x.divisors.card = 3) → S.card = 11
#[propext, Quot.sound, Classical.choice, sorryAx]
------------------
Replaying testNT.olean
Finished imports
Finished replay
---
theorem
mathd_numbertheory_221
∀ (S : Finset ℕ), (∀ (x : ℕ), x ∈ S ↔ 0 < x ∧ x < 1000 ∧ x.divisors.card = 3) → S.card = 11
#[propext, Quot.sound, Classical.choice]
Finished with no errors.

(targNT.olean contains the theorem statement with sorry in place of proof.)

[Kevin Buzzard]

Oxford was told that DeepSeek Prover may well have smashed SOTA but that we're still waiting for official confirmation from the PutnamBench people. I thought this was a pretty safe thing to say.

[Joseph Myers]

An accurate PutnamBench figure would require checking for each solved problem whether the solution indicates that the statement is correctly or incorrectly formalized, which might take a while.

To be fair to the AI, the problems it didn't solve likely also include some with mistakes in the formal statement that render it false. That probably isn't significant for a result of 49 out of 657 (current PutnamBench is probably a lot more accurate than the first release of CombiBench). But if you have a formal-to-formal benchmark where AIs are solving 80%-90%, or where you hope for benchmark results to be meaningful when they are at that level in future, this may be much more significant (in that 10% misformalized statements seems pretty good from experience for a benchmark, unless the authors formalized solutions to all the problems to get better accuracy than that).

[Oleg Murk]

GasStationManager said:

I backported SafeVerify to Lean 4.9.0 in the above-linked branch. Ran the deepseek solutions overnight. It found the problem with the apply?
https://github.com/GasStationManager/SafeVerify/tree/minif2f-deepseek-check

Potentially noob question: SafeVerify seems to reject proofs like this.

theorem two_plus_two_eq_four : 2 + 2 = 4 := by native_decide

->

uncaught exception: (kernel) unknown declaration 'two_plus_two_eq_four._nativeDecide_1'

Is this expected?

[Jason Rute]

@Oleg Murk native_decide doesn't go through the trusted kernel, but uses machine computation (which is less trusted) to do a proof by computation.

• It can be used to prove False if you don't use it carefully. See #general > Using `native_decide` to prove False?
• It uses additional axioms other than the standard three that SafeVerify checks for: propext, Quote.sound, and Classical.choice.
• It doesn't actually make a full proof term which can be replayed with the kernel, which is what lean4checker and (I believe) SafeVerify use to check that proofs are correct.

You can find a very recent conversation about this in #general > CombiBench : A benchmark focusing on combinatorics problem near the end of the conversation (over the previous few days).

[Jason Rute]

The conversation in that thread starts at #general > CombiBench : A benchmark focusing on combinatorics problem @ 💬 (although it also touches on other topics besides just native_decide).

[Ayush Agrawal]

Hi, I have few questions regarding DeepSeek-ProverV2:

GRPO training

• During the GRPO training, is DeepSeekV3 model and 7B model involved for generating the sketch and proving subgoals or these are just used for the cold start data collection?
• Is non-cot mode also used in the GRPO finetuning? Or is it just used for the expert iteration during the cold start?
• The authors mention the two stage pipeline. At a high level, first the model is trained in the non-cot mode and then it is trained with the cot mode right? Do we have an ablation that shows what is the importance of the stages apart from efficiency? What happens if we don't include non-cot stage at all? Also, what happens if we did GRPO finetuning with non-cot mode and not with the cot mode?
• Does the GRPO finetuning also includes the subgoals generated from the proofsketch as the additional problems? Or is it just used for the cold start? The authors mention that they include that in the expert iteration process. Is that only included for the non-cot mode?

Cold Start and Curriculum Learning

• Do we have the results of what happens with just DeepSeekV3 generating the proof sketch and 7B model as a prover on Minif2f test and Putnam-bench?
• At a high level, do we have an idea how much GRPO helps as compared to just cold start?
• "We curate a subset of challenging problems that remain unsolved by the 7B prover model in an end-to-end manner, but for which all decomposed subgoals have been successfully resolved"---What is this set? Authors have cited Ying 2024, Dong and Ma 2025, Lin 2025, minf2f valid, and DeepseekproverV1 dataset. Is there some other dataset used?

Misc

• The authors mentioned that 7B model proved some problems that bigger model didn't. Could it happen because of transfer of the initialised 1.5V model that was trained using MCTS search traces?
• What is the 7B prover model used for proving the decomposed lemmas? Is it DeepSeekProver-V1.5?

Thanks!

[Kelly Davis]

Ayush Agrawal said:

GRPO training

• During the GRPO training, is DeepSeekV3 model and 7B model involved for generating the sketch and proving subgoals or these are just used for the cold start data collection?

My guess upon reading section 2.3 Training Details of DeepSeek-Prover-V2 was that only the CoT data used for supervised fine-tuning was used for GRPO and no new data was created. However, they are silent on the data used.

The only reason I guess they only use the CoT data from supervised fine-tuning is that they state (1) "The CoT mode is enhanced through a further reinforcement learning stage..." and (2) "we curate (reinforcement learning) training prompts to include only problems sufficiently challenging yet solvable buy the supervised fine-tuned model".

At the point in the text where quote (2) appears, the only data (they mention) the supervised fine-tuned model has seen is the Cot and non-Cot data used for supervised fine-tuning.

But again this is just a guess.

• Is non-cot mode also used in the GRPO finetuning? Or is it just used for the expert iteration during the cold start?

For the reasons stated above I guess only CoT data is used for GRPO.

In particular they state "The CoT mode is enhanced through a further reinforcement learning stage...", which suggests that only CoT data is used for the GRPO reinforcement stage.

• The authors mention the two stage pipeline. At a high level, first the model is trained in the non-cot mode and then it is trained with the cot mode right? Do we have an ablation that shows what is the importance of the stages apart from efficiency? What happens if we don't include non-cot stage at all? Also, what happens if we did GRPO finetuning with non-cot mode and not with the cot mode?

My guess is that removing non-CoT training completely would materially effect the training pipeline as non-CoT data can be generated quicker, providing more training data thus speeding up the entire pipeline.

In particular, they state "The non-CoT generation mode is chosen to accelerate iterative training and data collection processes, as it offers significantly faster inference and validation cycles."

• Does the GRPO finetuning also includes the subgoals generated from the proofsketch as the additional problems? Or is it just used for the cold start? The authors mention that they include that in the expert iteration process. Is that only included for the non-cot mode?

I'd guess GRPO reinforcement learning doesn't include the subgoals.

As you mention, expert iteration includes subgoals. Expert iteration is also non-CoT as the Expert Iteration subsection of 2.3 Training Details of DeepSeek-Prover-V2 begins with:"The training procedure for the non-CoT mode of DeepSeek-Prover-V2 follows..." For the reasons mentioned above GRPO seems to be CoT only. So this suggests that GRPO isn't trained on subgoals.

Cold Start and Curriculum Learning

• Do we have the results of what happens with just DeepSeekV3 generating the proof sketch and 7B model as a prover on Minif2f test and Putnam-bench?

In the Proving Challenging Problems through Subgoal-guided Curricula subsection of 3.1. Results on MiniF2F Benchmark they state "Remarkably, our subgoal-guided curriculum learning framework, which integrates the general-purpose model DeepSeek-V3 with a lightweight specialized 7B prover, achieves a 90.2% success rate on miniF2F-valid, nearly matching the performance of DeepSeek-Prover-V2-671B."

Not really info on miniF2F-test, but I think this is suggestive of what one would expect from miniF2F-test.

Misc

• The authors mentioned that 7B model proved some problems that bigger model didn't.

I think these were due to the validation problems mentioned earlier in this thread?

All that said, I've no inside knowledge of DeepSeek, just the published texts. So, I'm reading tea leaves like everyone else.

[Ayush Agrawal]

Thanks a lot @Kelly Davis for sharing the insights you gained from the paper. It would have been great if the authors themselves clarify these things. It would be nice if others also share their insights!

[Jason Rute]

I don’t think we are going to hear from the authors. They haven’t responded to anything yet.

[Jason Rute]

Actually, @Huajian Xin might know the answers to @Ayush Agrawal’s questions.

[Huajian Xin]

Jason Rute said:

Actually, Huajian Xin might know the answers to Ayush Agrawal’s questions.

Sure! Here's a polished and professional English version of your message:

---

@Jason Rute Sorry, in V2 I only did some preliminary exploration and preparation on subgoal decomposition. The project that combined the 7B and 670B models was actually continued by my colleagues after I left, so I’m not very familiar with the specific details. The DeepSeek team rarely discusses things directly with the public, so we might not be able to learn much more.

As for the benchmark results, they are currently working with the benchmark maintainers to verify the findings. Once there are any updates, I’ll make sure to share them here as soon as possible :)

[George Tsoukalas]

Have now checked each proof submitted for the 49 problems from the team with https://github.com/GasStationManager/SafeVerify, and all passed. Parsing the proofs while looking at the informal proofs, I found that 2 of the 49 formalizations had slight bugs making them much easier than they should have been. After passing those corrected statements to the DeepSeek team, the new number (pass@1024) stands at 47/657 problems solved - a new SOTA (by far!) The proofs also admit much more complexity than I have seen from previous submissions to PutnamBench leaderboard. IMO, DeepSeekProverV2 is a step change improvement in AI for Math.

[Kevin Buzzard]

Excellent! Thanks for the update!

[Thomas Zhu]

@George Tsoukalas Are these the two formalization fixes?

[Jason Rute]

It looks like the DeepSeek-prover v2 paper was updated a few weeks ago. https://arxiv.org/abs/2504.21801 In particular, they wrote about the reward hacking bug. They also evaluated on CombiBench (by Numina), including giving an example of how their model was able to exploit an inconsistency in the hypotheses of a (now fixed?) CombiBench problem imosl_2011_c6 .

[GasStationManager]

@Jason Rute Thanks for checking! The updated version of the paper acknowledged (on page 10) that the 7B model used the bug to pass several of the PutnamBench problems. But also noted that the behavior is "noticeably absent in the outputs generated in the 671B version".

What about the apply? proof in the published MiniF2F solutions? I thought those were generated by the 671B version? The zip file has been updated along with the paper, and the file containing the offending proof (valid/algebra_amgm_prod1toneq1_sum1tongeqn) is now absent.

The paper's main claims regarding miniF2F are for the test split;
except for Table 2 (Problems solved by Deepseek-prover-v2-671B on miniF2F), in the column for miniF2F-valid, the row "Custom/Algebra" now reads 17/18 whereas the original version was 18/18.

That supports the hypothesis that the apply? proof in the original miniF2F solution zip was indeed generated by the 671B model.

[Mohamed Abdelatty]

Hello everyone :wave:,

I’m an undergraduate student in Computer Engineering at The British University in Egypt, and for my graduation project I will be working on a mathematical prover AI. I am very interested in building on DeepSeek-Prover-V2 because of its strong benchmarks on miniF2F and ProverBench.

I’ve already reviewed the GitHub repository and Hugging Face models, but I’m still unsure whether the full training/fine-tuning pipeline (especially the reinforcement learning and subgoal decomposition components) is available or if only inference/evaluation code is public. My goal is not to train from scratch, but to reproduce reported results and fine-tune on new problem sets.

Could anyone point me to the right resources, or confirm if the full pipeline is accessible? Any advice or tips for setting this up for a student graduation project would be greatly appreciated :folded_hands:.

Thanks in advance!

[Deleted User 968128]

This is a very broad set of questions and there are a lot of ways you can go here, which makes it tricky to answer.

Afaik DeepSeek has never provided any code around training or finetuning for any of their models.

Some resources to check out:

• https://fireworks.ai/models/fireworks/deepseek-prover-v2
• https://huggingface.co/haielab/DeepSeek-Prover-V2-7B-conjecture-base-FineTune-20250724_0955 (SFTtrainer finetuned, which is relatively straightforward to do)
• https://arxiv.org/abs/2502.07640 (and all Goedel related work)

o3-search and gpt5-search are great resources to find out more information on this topic.

[Mohamed Abdelatty]

Thanks a lot, Dr. @Tim Shephard :folded_hands:, this is very helpful. I’ll go through the resources you shared and explore the fine-tuning examples. It’s good to know that the full training/finetuning pipeline isn’t public, so I can adjust my expectations.

Would it be okay if I ask follow-up questions here in this topic if I run into issues or need clarification while trying things out?

[Jason Rute]

Reinforcement learning pipelines are not trivial to build, tune, or run. DeepSeek prover was likely built on the RL infrastructure of DeepSeek R1. You should look at that paper. Also this year there have been various papers going into even more detail on how to train LLMs with GRPO on verifiable rewards, both for theorem proving and for other tasks like math/code. For example, at Mistral we gave a lot of details in our Magistral paper: https://arxiv.org/abs/2506.10910

[Mohamed Abdelatty]

Thank you very much, Dr. @Jason Rute :folded_hands:. This is really helpful — I’ll take a closer look at the DeepSeek R1 paper and also read the Magistral paper for the GRPO details. I appreciate you pointing me to these directions.

If it’s okay, I might ask follow-up questions here after I’ve gone through them more carefully.

[Deleted User 968128]

Mohamed Abdelatty said:

I’ll take a closer look at the DeepSeek R1 paper and also read the Magistral paper for the GRPO details.

Note that in the Goedel paper I quoted above, the princeton team provides enough directions in the paper and especially appendix E for both DPO and GRPO finetuning of DS prover that can sufficiently drive gpt-5-codex (#Machine Learning for Theorem Proving > gpt-5-Codex is available on openrouter ) to implement their pipeline in its entirety. You will need to also supply the model config information and other data from the HF repo. Eg: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B/blob/main/config.json

image.png

You will ofc want to have gpt explain step by step how it all works, but that will be the enjoyable part of the task. This won't just be for your edification, but also because it is likely you will need to debug some issues you inevitably encounter with codex.

Your biggest blocker in this exercise will be paying for compute resources. You will want to first try to work with toy models of much lower parameter count and/or fast stopping until you are comfortable with what you have built. I use runpod.io as my goto for compute. But there is vast.ai and others. Kaggle and Colab provide free but limited compute.

To be clear: this task is reasonably cookbook (about 1-2 weeks FT work, ignoring $ and training time) but you might want to ask yourself what your novel contributions will be before setting out.

Another avenue you might want to look at is Retrieval Augmented Generation(RAG) and model context protocol (MCP). You can prove SOTA results in a faster, flexible manner with much less investment and work. It is also easier to share with others.

RAG will also have a longer shelf life and more valuable application as any SOTA work you do with RL will likely be eclipsed very soon. It can also enhance models like gpt-5-codex for true SOTA and not just DS-prover-7b.

The downside is that it is more about engineering and less theoretical.

Again, I always encourage consulting o3-search and gpt5-search early and often. Agentic search is the killer app of LLMs after coding.

[Mohamed Abdelatty]

Thank you so much, Dr. @Tim Shephard , this really clarifies the scope and challenges involved. After considering your advice, I realize that building and reproducing the full RL pipeline may be too ambitious for my graduation project, especially with the compute requirements.

I truly appreciate the time and detailed guidance you and Dr. @Jason Rute have shared with me — it has been very valuable in helping me understand the landscape better. I’ll likely pursue another topic that is more feasible for me as a student, but I’m grateful for what I’ve learned here.

[Mohamed Abdelatty]

Thank you very much,Dr. @Jason Rute , for pointing me toward the DeepSeek R1 paper and the Magistral work on GRPO. Your explanation really helped me understand how complex RL pipelines are and why they’re not trivial to reproduce.

After reflecting on your advice and Dr. @Tim Shephard , I think the RL direction may be too ambitious for my graduation project, given the time and compute required. I’m very grateful for the insights you’ve shared — they’ve given me a much clearer view of the research landscape, and that’s already been a big help for me.

[Deleted User 968128]

Mohamed Abdelatty said:

Thank you so much, Dr. Tim Shephard , this really clarifies the scope and challenges involved. After considering your advice, I realize that building and reproducing the full RL pipeline may be too ambitious for my graduation project, especially with the compute requirements.

My goal actually was not to discourage you, just to make you aware of compute costs, which can be reduced if you try a toy model.

Writing a cookbook RL pipeline is actually quite easy with the assistance of frontier models. The only ? really is how much you learn step by step what is happening.

[Deleted User 968128]

Here is an easy and fun project to play with to get started on RL .. you can get this up in a day with minimal compute and start adding and ablating to see how it changes behavior. https://gist.github.com/willccbb/4676755236bb08cab5f4e54a0475d6fb

A great deal of the LLM technology is actually surprisingly simple to re-implement once you've dived into it (it really is mostly matrix multiplication). The complexity is in the math behind it and the blocker is access to computes.