feat: Use aesop to solve for goals

examples_search/Example/lake-manifest.json

@@ -10,6 +10,15 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.8.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
@@ -19,15 +28,6 @@
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
@@ -55,7 +55,7 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "rev": "db651742f2c631e5b8525e9aabcf3d61ed094a4a",

examples_search/Example/lakefile.lean

@@ -1,8 +1,8 @@
 import Lake
 open Lake DSL
 
--- require aesop from git
+require aesop from git
---   "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
+  "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.8.0-rc1"

pantograph/search.py

@@ -73,6 +73,8 @@ class Agent:
             if search_state.is_solved:
                 # if the state is solved, propagate this solved status
                 if search_state.is_root:
+                    if verbose:
+                        print("Search complete: Root state solved")
                     self.reset()
                     return True
 

pantograph/search_llm.py

@@ -15,16 +15,11 @@ class LLMAgent(Agent):
         sgl.set_default_backend(sgl.OpenAI("gpt-4"))
 
         self.goal_tactic_id_map = collections.defaultdict(lambda : 0)
-        self.intros = [
-            "intro",
-        ]
         self.tactics = [
-            "simp",
+            "aesop",
-            "rfl",
+            #"simp",
-            "decide",
+            #"rfl",
-        ]
+            #"decide",
-        self.no_space_tactics = [
-            "assumption",
         ]
 
     def next_tactic(self, state: GoalState, goal_id: int, informal_stmt:str="",  informal_proof:str="") -> Optional[Tactic]:
@@ -32,13 +27,7 @@ class LLMAgent(Agent):
         i = self.goal_tactic_id_map[key]
 
         target = state.goals[goal_id].target
-        if target.startswith('∀'):
+        if i >= len(self.tactics):
-            tactics = self.intros
-        elif ' ' in target:
-            tactics = self.tactics
-        else:
-            tactics = self.no_space_tactics
-        if i >= len(tactics):
             new_state = None
             for ii in range(self.n_trials):
                 print(f"===============trail {str(ii)}============")
@@ -51,13 +40,9 @@ class LLMAgent(Agent):
                 if tactic:
                     return tactic
             return None
-    
         else:
             self.goal_tactic_id_map[key] = i + 1
-            return tactics[i]
+            return self.tactics[i]
-
-
-
 
 class TestSearch(unittest.TestCase):