[GH-ISSUE #18] Some ProofNet ground truth formalizations are incorrect #10

New issue

Open

opened 2026-10-26 21:06:34 +00:00 by bsakaguchi · 1 comment

bsakaguchi commented

2026-10-26 21:06:34 +00:00

Owner

Originally created by @jsimonrichard on GitHub (Mar 25, 2025).
Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/18

I found two theorems in your ProofNet dataset for LEAN 4 that have incorrect formalizations:

exercise_11_4_6b: Prove that x^1 + 1 is irreducible in \mathbb{F}_7. Formalization:

-- header
import Mathlib

open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd
open scoped BigOperators

-- theorem
theorem exercise_11_4_6b {F : Type*} [Field F] [Fintype F] (hF : card F = 31) :
  Irreducible (X ^ 3 - 9 : Polynomial F) :=

exercise_11_4_1b: Prove that x^3+6x+12 is irreducible in \mathbb{Q}. Formalization:

-- header
import Mathlib

open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd
open scoped BigOperators

-- theorem
theorem exercise_11_4_1b {F : Type*} [Field F] [Fintype F] (hF : card F = 2) : -- note the `hF` definition
  Irreducible (12 + 6 * X + X ^ 3 : Polynomial F) :=

I have yet to go through most of the theorems in ProofNet, but it raises the question---are there other errors like this, and how does that impact previous results using the ProofNet dataset?

Originally created by @jsimonrichard on GitHub (Mar 25, 2025). Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/18 I found two theorems in your ProofNet dataset for LEAN 4 that have incorrect formalizations: - **exercise_11_4_6b**: Prove that $x^1 + 1$ is irreducible in $\mathbb{F}_7$. Formalization: ```lean -- header import Mathlib open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd open scoped BigOperators -- theorem theorem exercise_11_4_6b {F : Type*} [Field F] [Fintype F] (hF : card F = 31) : Irreducible (X ^ 3 - 9 : Polynomial F) := ``` - **exercise_11_4_1b**: Prove that $x^3+6x+12$ is irreducible in $\mathbb{Q}$. Formalization: ```lean -- header import Mathlib open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd open scoped BigOperators -- theorem theorem exercise_11_4_1b {F : Type*} [Field F] [Fintype F] (hF : card F = 2) : -- note the `hF` definition Irreducible (12 + 6 * X + X ^ 3 : Polynomial F) := ``` I have yet to go through most of the theorems in ProofNet, but it raises the question---are there other errors like this, and how does that impact previous results using the ProofNet dataset?

bsakaguchi commented

2026-10-26 21:06:35 +00:00

Author

Owner

@0xA672 commented on GitHub (Jul 11, 2026):

I found two theorems in your ProofNet dataset for LEAN 4 that have incorrect formalizations:
exercise_11_4_6b: Prove that
x
1
1
is irreducible in
  F

7
. Formalization:
-- header
import Mathlib

open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd
open scoped BigOperators

-- theorem
theorem exercise_11_4_6b {F : Type*} [Field F] [Fintype F] (hF : card F = 31) :
Irreducible (X ^ 3 - 9 : Polynomial F) :=
exercise_11_4_1b: Prove that
x
3
6
x
+
12
is irreducible in
Q
. Formalization:
-- header
import Mathlib

open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd
open scoped BigOperators

-- theorem
theorem exercise_11_4_1b {F : Type*} [Field F] [Fintype F] (hF : card F = 2) : -- note the hF definition
Irreducible (12 + 6 * X + X ^ 3 : Polynomial F) :=
I have yet to go through most of the theorems in ProofNet, but it raises the question---are there other errors like this, and how does that impact previous results using the ProofNet dataset?

Thank you for the inspiration. I believe it would be very valuable to write a paper titled 'On the Fidelity of Neural Theorem Proving Benchmarks' :)

@0xA672 commented on GitHub (Jul 11, 2026): > I found two theorems in your ProofNet dataset for LEAN 4 that have incorrect formalizations: > > * **exercise_11_4_6b**: Prove that > > x > 1 > > + > 1 > is irreducible in > > > F > > 7 > > . Formalization: > > -- header > import Mathlib > > open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd > open scoped BigOperators > > -- theorem > theorem exercise_11_4_6b {F : Type*} [Field F] [Fintype F] (hF : card F = 31) : > Irreducible (X ^ 3 - 9 : Polynomial F) := > * **exercise_11_4_1b**: Prove that > > x > 3 > > + > 6 > x > + > 12 > is irreducible in > > Q > > . Formalization: > > -- header > import Mathlib > > open Function Fintype Subgroup Ideal Polynomial Submodule Zsqrtd > open scoped BigOperators > > -- theorem > theorem exercise_11_4_1b {F : Type*} [Field F] [Fintype F] (hF : card F = 2) : -- note the `hF` definition > Irreducible (12 + 6 * X + X ^ 3 : Polynomial F) := > I have yet to go through most of the theorems in ProofNet, but it raises the question---are there other errors like this, and how does that impact previous results using the ProofNet dataset? Thank you for the inspiration. I believe it would be very valuable to write a paper titled 'On the Fidelity of Neural Theorem Proving Benchmarks' :)

No labels

pull-request

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

deepseek-ai/DeepSeek-Prover-V1.5#10

No description provided.

Rows
Columns