运行quick_start.py但是报错，可能是lean4的问题？

[fixtech]

你好，首先非常感谢这个非常棒的开源工程的工作！我在按照安装说明安装好依赖和mathlib后，执行quick_start.py，但是并没有得到预期结果，NN模型有正确输出结果，但是lean4的验证有问题。
python quick_start.py
Special tokens have been added in the vocabulary, make sure the associated word embeddings are fine-tuned or trained.
INFO 10-21 23:04:38 llm_engine.py:98] Initializing an LLM engine (v0.4.1) with config: model='/data1/datasets/DeepSeek-Prover-V1.5-RL/', speculative_config=None, tokenizer='/data1/datasets/DeepSeek-Prover-V1.5-RL/', skip_tokenizer_init=False, tokenizer_mode=auto, revision=None, tokenizer_revision=None, trust_remote_code=True, dtype=torch.bfloat16, max_seq_len=4096, download_dir=None, load_format=auto, tensor_parallel_size=1, disable_custom_all_reduce=False, quantization=None, enforce_eager=False, kv_cache_dtype=auto, quantization_param_path=None, device_config=cuda, decoding_config=DecodingConfig(guided_decoding_backend='outlines'), seed=1)
Special tokens have been added in the vocabulary, make sure the associated word embeddings are fine-tuned or trained.
INFO 10-21 23:04:38 utils.py:608] Found nccl from library /root/.config/vllm/nccl/cu12/libnccl.so.2.18.1
INFO 10-21 23:04:39 selector.py:28] Using FlashAttention backend.
INFO 10-21 23:04:49 model_runner.py:173] Loading model weights took 12.8725 GB
INFO 10-21 23:04:51 gpu_executor.py:119] # GPU blocks: 7742, # CPU blocks: 546
INFO 10-21 23:05:00 model_runner.py:976] Capturing the model for CUDA graphs. This may lead to unexpected consequences if the model is not static. To run the model in eager mode, set 'enforce_eager=True' or use '--enforce-eager' in the CLI.
INFO 10-21 23:05:00 model_runner.py:980] CUDA graphs can take additional 1~3 GiB memory per GPU. If you are running out of memory, consider decreasing gpu_memory_utilization or enforcing eager mode. You can also reduce the max_num_seqs as needed to decrease memory usage.
INFO 10-21 23:05:12 model_runner.py:1057] Graph capturing finished in 12 secs.
Complete launching 1 LeanServerProcesses
Complete the following Lean 4 code:

import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- The second and fourth terms of a geometric sequence are $2$ and $6$. Which of the following is a possible first term?
Show that it is $\frac{2\sqrt{3}}{3}$.-/
theorem amc12b_2003_p6 (a r : ℝ) (u : ℕ → ℝ) (h₀ : ∀ k, u k = a * r ^ k) (h₁ : u 1 = 2)
  (h₂ : u 3 = 6) : u 0 = 2 / Real.sqrt 3 ∨ u 0 = -(2 / Real.sqrt 3) := by
  simp_all only [Nat.one_eq_succ_zero, Nat.zero_eq, zero_add, Nat.add_succ, Nat.add_zero,
    Nat.succ_add]
  have h₁' : a * r = 2 := by simpa [h₀] using h₁
  have h₂' : a * r ^ 3 = 6 := by simpa [h₀] using h₂
  have h₃ : r ^ 2 = 3 := by
    nlinarith
  have h₄ : a = 2 / Real.sqrt 3 ∨ a = -(2 / Real.sqrt 3) := by
    apply eq_or_eq_neg_of_sq_eq_sq <;>
    field_simp <;>
    nlinarith
  simpa [h₀] using h₄

{"cmd": "import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n/-- The second and fourth terms of a geometric sequence are $2$ and $6$. Which of the following is a possible first term?\nShow that it is $\frac{2\sqrt{3}}{3}$.-/\ntheorem amc12b_2003_p6 (a r : ℝ) (u : ℕ → ℝ) (h₀ : ∀ k, u k = a * r ^ k) (h₁ : u 1 = 2)\n (h₂ : u 3 = 6) : u 0 = 2 / Real.sqrt 3 ∨ u 0 = -(2 / Real.sqrt 3) := by\n simp_all only [Nat.one_eq_succ_zero, Nat.zero_eq, zero_add, Nat.add_succ, Nat.add_zero,\n Nat.succ_add]\n have h₁' : a * r = 2 := by simpa [h₀] using h₁\n have h₂' : a * r ^ 3 = 6 := by simpa [h₀] using h₂\n have h₃ : r ^ 2 = 3 := by\n nlinarith\n have h₄ : a = 2 / Real.sqrt 3 ∨ a = -(2 / Real.sqrt 3) := by\n apply eq_or_eq_neg_of_sq_eq_sq <;>\n field_simp <;>\n nlinarith\n simpa [h₀] using h₄", "allTactics": false, "ast": false, "tactics": false, "premises": false}
{'pass': False, 'complete': False, 'system_errors': 'Traceback (most recent call last):\n File "/data/06_prover/DeepSeek-Prover-V1.5/prover/lean/verifier.py", line 42, in verify_lean4_file\n result = json.loads(outputs.stdout)\n File "/data1/anaconda/envs/prover/lib/python3.10/json/init.py", line 346, in loads\n return _default_decoder.decode(s)\n File "/data1/anaconda/envs/prover/lib/python3.10/json/decoder.py", line 337, in decode\n obj, end = self.raw_decode(s, idx=_w(s, 0).end())\n File "/data1/anaconda/envs/prover/lib/python3.10/json/decoder.py", line 355, in raw_decode\n raise JSONDecodeError("Expecting value", s, err.value) from None\njson.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)\n', 'system_messages': '', 'verify_time': 0.9813518524169922}
All 1 LeanServerProcesses stopped

[xinhjBrant]

是的，这说明Lean server没有返回任何内容，请检查Lean server的安装

[Edmund-Lai]

I ran into the same issue and found a solution, I hope it helps:

1. First, check if lake exe repl runs correctly:

cd mathlib4
lake exe repl

If it doesn’t run, the problem might be with lake. In that case, double-check the Lean4 installation to ensure everything was set up properly.

2. Next, check the run method in class Lean4ServerProcess. This part of the code sets a limit on resource usage. I was able to get it working by commenting out that section.