deepseek-ai/DeepSeek-Prover-V1.5
1
0
Fork 0
mirror of https://github.com/deepseek-ai/DeepSeek-Prover-V1.5.git synced 2026-11-05 00:57:20 +00:00
Code Issues 12 Projects Packages Wiki Activity

[GH-ISSUE #4] Simple theorem generates "Cannot parse a sorry tactic on root." Error #2

New issue
Closed
opened 2026-10-26 21:06:28 +00:00 by bsakaguchi · 4 comments
bsakaguchi commented 2026-10-26 21:06:28 +00:00
Owner
Copy link

Originally created by @sethahrenbach on GitHub (Aug 28, 2024).
Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/4

My theorem file:

{"name": "binaryAdditionLength", "split": "valid", "informal_prefix": "/-- Let `binaryAddition` be a function that takes two lists of booleans, each representing a binary number of at most 10 bits, and returns a list of booleans representing their sum modulo 1024. Prove that the length of the output is at most 10 bits. -/\n", "formal_statement": "theorem binaryAdditionLength (s t : List Bool) :\n  (binaryAddition s t).length ≤ 10 :=", "goal": "s t : List Bool\n⊢ (binaryAddition s t).length ≤ 10", "header": "def binaryAddition (s t : List Bool) : List Bool :=\n  let rec loop (i : Nat) (carry : Bool) (acc : List Bool) : List Bool :=\n    match s.get? i, t.get? i with\n    | some a, some b => \n        let sum := (if a then 1 else 0) + (if b then 1 else 0) + (if carry then 1 else 0)\n        loop (i+1) (sum ≥ 2) ((sum % 2 = 1) :: acc)\n    | some a, none => \n        let sum := (if a then 1 else 0) + (if carry then 1 else 0)\n        loop (i+1) (sum = 2) ((sum % 2 = 1) :: acc)\n    | none, some b => \n        let sum := (if b then 1 else 0) + (if carry then 1 else 0)\n        loop (i+1) (sum = 2) ((sum % 2 = 1) :: acc)\n    | none, none => \n        if carry then true::acc else acc\n  termination_by _ i _ _ => (max s.length t.length) - i\n  (loop 0 false []).reverse.take 10\n\n"}

As you can see it requires no imports and does not contain any sorry tactics.

Originally created by @sethahrenbach on GitHub (Aug 28, 2024). Original GitHub issue: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5/issues/4 My theorem file: ``` {"name": "binaryAdditionLength", "split": "valid", "informal_prefix": "/-- Let `binaryAddition` be a function that takes two lists of booleans, each representing a binary number of at most 10 bits, and returns a list of booleans representing their sum modulo 1024. Prove that the length of the output is at most 10 bits. -/\n", "formal_statement": "theorem binaryAdditionLength (s t : List Bool) :\n (binaryAddition s t).length ≤ 10 :=", "goal": "s t : List Bool\n⊢ (binaryAddition s t).length ≤ 10", "header": "def binaryAddition (s t : List Bool) : List Bool :=\n let rec loop (i : Nat) (carry : Bool) (acc : List Bool) : List Bool :=\n match s.get? i, t.get? i with\n | some a, some b => \n let sum := (if a then 1 else 0) + (if b then 1 else 0) + (if carry then 1 else 0)\n loop (i+1) (sum ≥ 2) ((sum % 2 = 1) :: acc)\n | some a, none => \n let sum := (if a then 1 else 0) + (if carry then 1 else 0)\n loop (i+1) (sum = 2) ((sum % 2 = 1) :: acc)\n | none, some b => \n let sum := (if b then 1 else 0) + (if carry then 1 else 0)\n loop (i+1) (sum = 2) ((sum % 2 = 1) :: acc)\n | none, none => \n if carry then true::acc else acc\n termination_by _ i _ _ => (max s.length t.length) - i\n (loop 0 false []).reverse.take 10\n\n"} ``` As you can see it requires no imports and does not contain any `sorry` tactics.
bsakaguchi commented 2026-10-26 21:06:29 +00:00
Author
Owner
Copy link

@sethahrenbach commented on GitHub (Aug 28, 2024):

Looks like a syntax error in the header content will trigger the sorry error. It would be useful to have the syntax errors surfaced.

<!-- gh-comment-id:2315704028 --> @sethahrenbach commented on GitHub (Aug 28, 2024): Looks like a syntax error in the `header` content will trigger the `sorry` error. It would be useful to have the syntax errors surfaced.
bsakaguchi commented 2026-10-26 21:06:29 +00:00
Author
Owner
Copy link

@fzyzcjy commented on GitHub (Aug 29, 2024):

+1 I see

Process SearchProcess-38:
Traceback (most recent call last):
  File "/opt/conda/lib/python3.11/multiprocessing/process.py", line 314, in _bootstrap
    self.run()
  File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/workers/search.py", line 66, in run
    for sample, info in sample_generator:
  File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 267, in sample
    self.root, sample_count, yield_cache = self._tree_setup(data)
                                           ^^^^^^^^^^^^^^^^^^^^^^
  File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 167, in _tree_setup
    assert root_sorry.result['pass'], "Cannot parse a `sorry` tactic on root."
AssertionError: Cannot parse a `sorry` tactic on root.
<!-- gh-comment-id:2317043735 --> @fzyzcjy commented on GitHub (Aug 29, 2024): +1 I see ``` Process SearchProcess-38: Traceback (most recent call last): File "/opt/conda/lib/python3.11/multiprocessing/process.py", line 314, in _bootstrap self.run() File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/workers/search.py", line 66, in run for sample, info in sample_generator: File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 267, in sample self.root, sample_count, yield_cache = self._tree_setup(data) ^^^^^^^^^^^^^^^^^^^^^^ File "/host_home/research/code/third_party_inline/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 167, in _tree_setup assert root_sorry.result['pass'], "Cannot parse a `sorry` tactic on root." AssertionError: Cannot parse a `sorry` tactic on root. ```
bsakaguchi commented 2026-10-26 21:06:29 +00:00
Author
Owner
Copy link

@saisurbehera commented on GitHub (Sep 1, 2024):

+1, has anyone found a fix for this

AssertionError: Cannot parse a `sorry` tactic on root.
Process SearchProcess-327:
Traceback (most recent call last):
  File "/root/miniconda3/lib/python3.12/multiprocessing/process.py", line 314, in _bootstrap
    self.run()
  File "/root/DeepSeek-Prover-V1.5/prover/workers/search.py", line 64, in run
    for sample, info in sample_generator:
  File "/root/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 267, in sample
    self.root, sample_count, yield_cache = self._tree_setup(data)
                                           ^^^^^^^^^^^^^^^^^^^^^^
  File "/root/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 167, in _tree_setup
    assert root_sorry.result['pass'], "Cannot parse a `sorry` tactic on root."
<!-- gh-comment-id:2323487814 --> @saisurbehera commented on GitHub (Sep 1, 2024): +1, has anyone found a fix for this ``` AssertionError: Cannot parse a `sorry` tactic on root. Process SearchProcess-327: Traceback (most recent call last): File "/root/miniconda3/lib/python3.12/multiprocessing/process.py", line 314, in _bootstrap self.run() File "/root/DeepSeek-Prover-V1.5/prover/workers/search.py", line 64, in run for sample, info in sample_generator: File "/root/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 267, in sample self.root, sample_count, yield_cache = self._tree_setup(data) ^^^^^^^^^^^^^^^^^^^^^^ File "/root/DeepSeek-Prover-V1.5/prover/algorithms/rmax_tree_search.py", line 167, in _tree_setup assert root_sorry.result['pass'], "Cannot parse a `sorry` tactic on root." ```
bsakaguchi commented 2026-10-26 21:06:29 +00:00
Author
Owner
Copy link

@longdct commented on GitHub (Sep 24, 2024):

This bug was caused by REPL dependency of mathlib4. I removed that package and built it again, and it worked.

cd mathlib4
rm -rf .lake/packages/REPL/
lake build REPL
<!-- gh-comment-id:2369922679 --> @longdct commented on GitHub (Sep 24, 2024): This bug was caused by REPL dependency of mathlib4. I removed that package and built it again, and it worked. ``` cd mathlib4 rm -rf .lake/packages/REPL/ lake build REPL ```
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
No results found.
Labels
Clear labels   
pull-request
Mirrored from GitHub Pull Request

No labels
pull-request
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
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#2
No description provided.