From 4f3397fd82fef0a4dc5c3a8bf5993500f078a6cd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 5 Jun 2024 11:19:43 -0700 Subject: [PATCH] chore: Remove unused code --- examples_search/miniF2F_search.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/examples_search/miniF2F_search.py b/examples_search/miniF2F_search.py index 74d1cbc..3c57019 100755 --- a/examples_search/miniF2F_search.py +++ b/examples_search/miniF2F_search.py @@ -31,7 +31,5 @@ if __name__ == '__main__': test_data = read_test_data() server = Server(imports=["Mathlib"], project_path=project_path, lean_path=lean_path) - target = "∀ (b h v : ℝ) (h₀ : 0 < b ∧ 0 < h ∧ 0 < v) (h₁ : v = 1 / 3 * (b * h)) (h₂ : b = 30) (h₃ : h = 13 / 2) , v = 65" - # target = "theorem mathd_algebra_478\n (b h v : ℝ)\n (h₀ : 0 < b ∧ 0 < h ∧ 0 < v)\n (h₁ : v = 1 / 3 * (b * h))\n (h₂ : b = 30)\n (h₃ : h = 13 / 2) :\n v = 65 := sorry" agent = LLMAgent(server) try_test_data(server, agent, test_data[0])