[GH-ISSUE #26] Statement defects in datasets/minif2f.jsonl, and passes on them in released V2 solutions #14

New issue

Open

opened 2026-10-26 21:06:36 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

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

Owner

Originally created by @fabio-rovai on GitHub (Sep 13, 2026).
Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/26

Hello,

While auditing circulating miniF2F copies I found the following in your artifacts. All
items are machine-verified under Lean 4.9 (your era) and reproduce from public files.

datasets/minif2f.jsonl (V1.5 repo) carries five statements whose big-operator body
is unparenthesised, so the binder variable escapes: induction_pord1p1on2powklt5on2,
induction_prod1p1onk3le3m1onn, amc12a_2021_p9, mathd_algebra_158, mathd_algebra_342.
Under autoImplicit these elaborate with a phantom universally quantified variable; the
elaborated signatures show it. mathd_algebra_158 as shipped is vacuously true: its
hypotheses are contradictory (parity argument, omega-checkable).
The same file states mathd_algebra_314 without the real-type ascription; over N the
statement is 0 = 0. Your V2 release's minif2f-solutions.zip contains a proof of it
whose first step is have h1 : 1 / 4 = 0, and a proof of induction_pord whose first
step evaluates a product of ones, confirming the degenerate parse. Both are counted in
the released solution set.
The Goedel-Prover-V2 repository ships a copy of the same file with 15 of these
statements silently repaired, so results across the two lineages are not computed on
the same benchmark.

Also for awareness: the Lean Workbook corpus contains 23 statements with the same
phantom-variable defect (list available), relevant to training-data quality.

Reproduction scripts available on request.

Originally created by @fabio-rovai on GitHub (Sep 13, 2026). Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/26 Hello, While auditing circulating miniF2F copies I found the following in your artifacts. All items are machine-verified under Lean 4.9 (your era) and reproduce from public files. 1. datasets/minif2f.jsonl (V1.5 repo) carries five statements whose big-operator body is unparenthesised, so the binder variable escapes: induction_pord1p1on2powklt5on2, induction_prod1p1onk3le3m1onn, amc12a_2021_p9, mathd_algebra_158, mathd_algebra_342. Under autoImplicit these elaborate with a phantom universally quantified variable; the elaborated signatures show it. mathd_algebra_158 as shipped is vacuously true: its hypotheses are contradictory (parity argument, omega-checkable). 2. The same file states mathd_algebra_314 without the real-type ascription; over N the statement is 0 = 0. Your V2 release's minif2f-solutions.zip contains a proof of it whose first step is `have h1 : 1 / 4 = 0`, and a proof of induction_pord whose first step evaluates a product of ones, confirming the degenerate parse. Both are counted in the released solution set. 3. The Goedel-Prover-V2 repository ships a copy of the same file with 15 of these statements silently repaired, so results across the two lineages are not computed on the same benchmark. Also for awareness: the Lean Workbook corpus contains 23 statements with the same phantom-variable defect (list available), relevant to training-data quality. Reproduction scripts available on request.

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#14

No description provided.

Rows
Columns