upgrade to lean 4

lean-dojo · Mar 16, 2024 · d255d07 · d255d07
1 parent c5401d4
commit d255d07
Show file tree

Hide file tree

Showing 6 changed files with 1 addition and 1,511 deletions.
diff --git a/docs/eval_MiniF2F_ProofNet.md b/docs/eval_MiniF2F_ProofNet.md
diff --git a/generator/model.py b/generator/model.py
@@ -371,7 +371,7 @@ def __init__(
         openai.organization = organization
         openai.api_key = api_key
         self.model = model
-        self.default_prompt = "You are an expert in Lean3 theorem proofs. We are trying to solve the Lean3 theorem 'THEOREM_FULL_NAME' from the mathlib file 'FILE_PATH'. The current tactic state is: 'TACTIC_STATE'. Suggest exactly NUM_SAMPLES unique tactics to progress in solving 'THEOREM_FULL_NAME', along with their confidence levels as a float between 0 and 1. Rank them in order of effectiveness. Present the tactics and their confidence levels as comma-separated tuples in this format: #(tactic_{1}, confidence_{1})#, #(tactic_{2}, confidence_{2})#, ..., #(tactic_{NUM_SAMPLES}, confidence_{NUM_SAMPLES})#."
+        self.default_prompt = "You are an expert in theorem proving in Lean. We are trying to solve the Lean theorem 'THEOREM_FULL_NAME' from the mathlib file 'FILE_PATH'. The current tactic state is: 'TACTIC_STATE'. Suggest exactly NUM_SAMPLES unique tactics to progress in solving 'THEOREM_FULL_NAME', along with their confidence levels as a float between 0 and 1. Rank them in order of effectiveness. Present the tactics and their confidence levels as comma-separated tuples in this format: #(tactic_{1}, confidence_{1})#, #(tactic_{2}, confidence_{2})#, ..., #(tactic_{NUM_SAMPLES}, confidence_{NUM_SAMPLES})#."
         self.max_tokens = max_tokens
         self.num_retries = num_retries
         self.threshold = threshold