How to set the prompt when trying to get the first line of proof

[bhwangfy]

Thanks for this great work! I am trying to play with the model:

1. as mentioned in the paper (internlm2.5 step prover), the prompt consists of theorem name, proof before, and tactic state. I wonder how the "proof before" is set when there is no line of proof currently (i.e., we have just started to prove)? Also, is the "proof before" only the last line of proof, or the total proof?

2. there are scenarios where the model can generate multiple lines of code, here should we only use the first line of code or just all the codes?

Thanks for your time!

[wzj423]

Thank you for your question. Here are the details:

1. If there is no line of proof, you can leave that field empty. For example:
   ---\nNAME: algebra_sqineq_unitcircatbpabsamblt1\n\n---\nPROOF_BEFORE: \n\n---\nSTATE_BEFORE: a b : ℝ\nh₀ : a ^ 2 + b ^ 2 = 1\n⊢ a * b + |a - b| ≤ 1\n\n---\nTACTIC:

2. In our experiments, we utilize all the code. It's possible for the model to generate an indented code block that spans multiple lines. An example of this can be seen in the introduction of hypothesis h4 in our mathd_algebra_31 case study:
   

I hope this helps!

[bhwangfy]

Thanks for your quick response and this helps a lot! To confirm, by referring to the hypothesis h4 example, you mean that the model generates all the code at once from "have h4: ..." to "... rw [h_0]" right? If yes, that makes sense to me. Thanks!

[wzj423]

Yes, exactly.