wip

examples_search/Example/.gitignore

@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*

examples_search/Example/Example.lean

@@ -0,0 +1,3 @@
+import Import.Mathlib
+
+-- Ensure that Aesop is running

examples_search/Example/lake-manifest.json

@@ -0,0 +1,23 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "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"}],
+ "name": "Example",
+ "lakeDir": ".lake"}

examples_search/Example/lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+open Lake DSL
+
+require aesop from git
+  "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
+
+package Example
+
+@[default_target]
+lean_lib Example

examples_search/Example/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1

examples_search/README.md

@@ -0,0 +1,15 @@
+# Usage Example
+
+This example showcases how to bind library dependencies and execute the `Aesop`
+tactic in Lean. First build the example project:
+``` sh
+pushd Example
+lake build
+popd
+```
+This would generate compiled `.olean` files. Then run the example from the
+project root:
+``` sh
+poetry run examples/aesop.py
+```
+

examples_search/aesop.py

@@ -0,0 +1,19 @@
+#!/usr/bin/env python3
+
+import subprocess
+from pathlib import Path
+from pantograph.server import Server
+
+def get_project_and_lean_path():
+    cwd = Path(__file__).parent.resolve() / 'Example'
+    p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)
+    return cwd, p
+
+if __name__ == '__main__':
+    project_path, lean_path = get_project_and_lean_path()
+    print(f"$PWD: {project_path}")
+    print(f"$LEAN_PATH: {lean_path}")
+    server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
+    state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
+    state1 = server.goal_tactic(state0, goal_id=0, tactic="aesop")
+    assert state1.is_solved

examples_search/compile-tactics.py

@@ -0,0 +1,19 @@
+#!/usr/bin/env python3
+
+import subprocess
+from pathlib import Path
+from pantograph.server import Server
+
+def get_project_and_lean_path():
+    cwd = Path(__file__).parent.resolve() / 'Example'
+    p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)
+    return cwd, p
+
+if __name__ == '__main__':
+    project_path, lean_path = get_project_and_lean_path()
+    print(f"$PWD: {project_path}")
+    print(f"$LEAN_PATH: {lean_path}")
+    server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
+    data = server.compile_tactics("Example")
+    for (before, tactic, after) in data:
+        print(f"{before}\n{tactic}\n{after}\n\n")

pantograph/gen_tactic.py

@@ -90,7 +90,7 @@ def multi_turn_question(s, question_1, question_2):
 @sgl.function
 def select_tactic(s, server, state, goal_id, feedback_turns = 5):
     
-    s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.")
+    s += sgl.system("You are an expert in Lean. Choose the next ONE tactic to run given the current proof state and goals.")
     s += sgl.user(LEAN4_REWRITE)
     s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])")
     s += sgl.assistant("```intros a b h```")

pantograph/search_llm.py

@@ -59,20 +59,33 @@ class LLMAgent(Agent):
         return tactics[i]
 
 class TestSearch(unittest.TestCase):
-
-    def test_solve(self):
-
+    
+    def test_miniF2F(self):
+        problem = {"id": "mathd_algebra_478", 
+                   "split": "test", 
+                   "formal_statement": "theorem mathd_algebra_478\n  (b h v : \u211d)\n  (h\u2080 : 0 < b \u2227 0 < h \u2227 0 < v)\n  (h\u2081 : v = 1 / 3 * (b * h))\n  (h\u2082 : b = 30)\n  (h\u2083 : h = 13 / 2) :\n  v = 65 := sorry", 
+                   "header": "import Mathlib.Algebra.BigOperators.Basic\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\n\nopen BigOperators\nopen Real\nopen Nat\nopen Topology", 
+                   "informal_stmt": "The volume of a cone is given by the formula $V = \\frac{1}{3}Bh$, where $B$ is the area of the base and $h$ is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume? Show that it is 65.", 
+                   "informal_proof": "We are given that $B = 30$ and $h = 6.5$ and asked to find $\\frac{1}{3}Bh$.  We find that \\[\\frac{1}{3}Bh = \\frac{1}{3}(30)(6.5) = (10)(6.5) = 65.\\]"}
         server = Server()
         agent = LLMAgent(server)
-        flag = agent.search(server=server, target="∀ (p q: Prop), p -> p", verbose=True)
-        #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
+        flag = agent.search(server=server, target=" (b h v : \u211d)\n  (h\u2080 : 0 < b \u2227 0 < h \u2227 0 < v)\n  (h\u2081 : v = 1 / 3 * (b * h))\n  (h\u2082 : b = 30)\n  (h\u2083 : h = 13 / 2) :\n  v = 65", verbose=True)
         self.assertTrue(flag)
-    def test_solve_big(self):
 
-        server = Server()
-        agent = LLMAgent(server)
-        flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
-        self.assertTrue(flag)
+        
+    # def test_solve(self):
+
+    #     server = Server()
+    #     agent = LLMAgent(server)
+    #     flag = agent.search(server=server, target="∀ (p q: Prop), p -> p", verbose=True)
+    #     #flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
+    #     self.assertTrue(flag)
+    # def test_solve_big(self):
+
+    #     server = Server()
+    #     agent = LLMAgent(server)
+    #     flag = agent.search(server=server, target="∀ (p q: Prop), Or p q -> Or q p", verbose=True)
+    #     self.assertTrue(flag)
 
 
 if __name__ == '__main__':