Cases/induction in Single-Step Tactic generation LLM

Stream: Machine Learning for Theorem Proving

[sicheng tan]

I recently read some work on LLM Lean proof generation. Some works such as ReProver and DeepSeek-Prover-V1.5 generate one-step tactics and then combine them into a complete proof through search methods. But when I practiced, I found that there might be some problems when dealing with tactics such as cases and induction. For example:

theorem list_length_nonneg {α : Type} (xs : List α) : 0 ≤ xs.length := by
  induction xs with
  | nil => simp
--  | cons head tail ih =>
    -- simp
    -- exact Nat.zero_le _

REPL reports error : alternative 'cons' has not been provided
When only some cases are generated for a large model, the REPL verification will fail due to errors. In my opinion, these works will be verified by lean after generating tactics, and will be filtered when errors occur (but for cases/inductions, the proof can be completed if it continues). How do these works like ReProver handle the situation where LLM gradually generates cases and inductions and verify these tactics in detail?

[sicheng tan]

I think it shouldn't be filtered because of REPL errors. Do I just need to specially handle this case's error like alternative 'cons' has not been provided to let LLM generate next tactic?
Additional Notes：When I change code to:

theorem list_length_nonneg {α : Type} (xs : List α) : 0 ≤ xs.length := by
  induction xs with
  | nil => simp
 | cons head tail ih =>
    -- simp
    -- exact Nat.zero_le _

It only report unsolved goals. This will let LLM to generate tactic continuely until finish proof.

[(deleted)]

I don't quite understand. You should run LLMs yourself to see how they deal with this issue.