{"data":{"slug":"loganrjmurphy-leaneuclid","name":"LeanEuclid","tagline":"Benchmark for autoformalization in Euclidean geometry targeting Lean proof assistant.","github_url":"https://github.com/loganrjmurphy/LeanEuclid","owner":"loganrjmurphy","repo":"LeanEuclid","owner_avatar_url":"https://avatars.githubusercontent.com/u/35403042?v=4","primary_language":"Lean","stars":141,"forks":20,"topics":["autoformalization","euclidean-geometry","formalization","lean4","llm-evaluation","theorem-proving"],"archived":false,"github_pushed_at":"2026-08-10T15:52:30+00:00","maintenance_label":"Steady","stars_delta_30d":2,"url":"https://www.graphcanon.com/tools/loganrjmurphy-leaneuclid","markdown_url":"https://www.graphcanon.com/tools/loganrjmurphy-leaneuclid.md","api_url":"https://www.graphcanon.com/api/graphcanon/tools/loganrjmurphy-leaneuclid","graph_url":"https://www.graphcanon.com/api/graphcanon/graph?tool=loganrjmurphy-leaneuclid","description":"LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.","homepage_url":"http://arxiv.org/abs/2405.17216","license":"MIT","open_issues":6,"watchers":6,"ai_summary":"LeanEuclid is a benchmark focusing on the domain of Euclidean geometry, aimed at testing and advancing autoformalization techniques within the context of the Lean proof assistant. It assesses capabilities related to automated theorem proving and formal verification in geometric contexts.","readme_excerpt":"## Requirements\n\n* A working setup of [Lean 4](https://lean-lang.org/), including [elan](https://github.com/leanprover/elan) and [Lean's VSCode extension](https://lean-lang.org/lean4/doc/quickstart.html)\n* Install the latest version of [Z3](https://github.com/Z3Prover/z3) and [CVC5](https://cvc5.github.io/) and make sure they can be accessed from the command line\n* Install Python dependencies: `pip install smt-portfolio openai`\n* Find out the location of `smt-portfolio` and make sure Lean's VSCode extension can also access it. For example, if `which smt-portfolio` outputs `/Users/yangky/miniconda3/envs/lean/bin/smt-portfolio`, you should set `Server Env Paths` in Lean's VSCode extension as below:\n\"image\"","github_created_at":"2024-05-27T03:14:02+00:00","created_at":"2026-07-11T12:02:35.340322+00:00","updated_at":"2026-09-20T07:01:12.971726+00:00","categories":[{"slug":"evaluation-observability","name":"Evaluation & Observability","url":"https://www.graphcanon.com/categories/evaluation-observability","markdown_url":"https://www.graphcanon.com/categories/evaluation-observability.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/evaluation-observability"}],"tags":[{"slug":"autoformalization","name":"autoformalization"},{"slug":"euclidean-geometry","name":"euclidean-geometry"},{"slug":"formalization","name":"formalization"},{"slug":"lean4","name":"lean4"},{"slug":"llm-evaluation","name":"llm-evaluation"},{"slug":"theorem-proving","name":"theorem-proving"}],"trust":{"provenance":{"is_fork":false,"github_id":806353877,"owner_type":"User","methodology":"github_public_v1","parent_repo":null,"near_duplicate_slugs":[]},"computed_at":"2026-09-20T07:01:10.757Z","maintenance":{"label":"Steady","score":60,"methodology":"github_public_v1","releases_90d":0,"days_since_push":40,"last_release_at":null,"stars_delta_30d":2,"open_issues_delta_30d":1},"security_summary":{"status":"no_lockfile","scanner":null,"low_count":0,"high_count":0,"last_scan_at":"2026-07-11T12:02:39.658Z","medium_count":0,"scan_profile":"none","critical_count":0}},"capability_facts":{"scan":{"source":"repo_scan","observed_at":"2026-09-20T07:01:11.802Z"},"deploy":{"source":"dockerfile:Dockerfile","self_host":true,"observed_at":"2026-09-20T07:01:11.802Z","managed_saas":false},"languages":{"value":["lean"],"source":"github.language","observed_at":"2026-09-20T07:01:11.802Z"},"has_docker":{"value":true,"source":"dockerfile:Dockerfile","observed_at":"2026-09-20T07:01:11.802Z"},"license_spdx":{"value":"MIT","source":"github.license","observed_at":"2026-09-20T07:01:11.802Z"}},"decision_facts":{"hosting":null,"pricing":null,"requirements":{"notes":["Requires a fully functional setup with Lean 4, including elan and Lean's VSCode extension","Installation of Z3 and CVC5 solvers is mandatory for effective use","Python dependencies such as `smt-portfolio` and `openai` need to be installed via pip","Setting up server environment paths in Lean’s VSCode extension correctly is essential for tool functionality"],"min_ram_gb":null,"requires_docker":false},"constraints":{"min_ram_gb":null,"requires_docker":false},"when_to_use":["When you are specifically interested in advancing or testing automated theorem proving and formal verification techniques in Euclidean geometry using Lean 4","If your project explicitly requires integration with Lean 4, and particularly when leveraging tools like Z3 and CVC5 for solving SMT problems alongside autoformalization tasks"],"when_not_to_use":["Avoid if you are working within a different proof assistant ecosystem unrelated to Lean 4","Not suitable for benchmarking or developing autoformalization techniques outside the domain of Euclidean geometry"],"source":"enrich:decision_facts","observed_at":"2026-07-12T15:09:53.071Z"},"constraint_facets":{"min_ram_gb":null,"requires_docker":false},"decision_summary":[{"label":"Requirements","value":"Requires a fully functional setup with Lean 4, including elan and Lean's VSCode extension; Installation of Z3 and CVC5 solvers is mandatory for effective use; Python dependencies such as `smt-portfolio` and `openai` need to be installed via pip; Setting up server environment paths in Lean’s VSCode extension correctly is essential for tool functionality"},{"label":"Adopt for","value":"Decision-relevant specifics for LeanEuclid, a benchmark tailored for autoformalization in Euclidean geometry within the Lean proof assistant ecosystem."}]}}