{"data":{"slug":"loganrjmurphy-leaneuclid","name":"LeanEuclid","tagline":"LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.","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":136,"forks":17,"topics":["autoformalization","euclidean-geometry","formalization","lean4","llm-evaluation","theorem-proving"],"archived":false,"github_pushed_at":"2025-11-25T23:43:05+00:00","maintenance_label":"Slowing","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":5,"watchers":6,"ai_summary":null,"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<img width=\"938\" alt=\"image\" src=\"https://github.com/loganrjmurphy/LeanEuclid/assets/5431913/abfc6d25-e2e4-462e-934d-a10b4cb4e96c\">","github_created_at":"2024-05-27T03:14:02+00:00","created_at":"2026-07-11T12:02:35.340322+00:00","updated_at":"2026-07-12T03:45:18.388008+00:00","categories":[{"slug":"computer-vision","name":"Computer Vision","url":"https://www.graphcanon.com/categories/computer-vision","markdown_url":"https://www.graphcanon.com/categories/computer-vision.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/computer-vision"},{"slug":"developer-tools","name":"Developer Tools","url":"https://www.graphcanon.com/categories/developer-tools","markdown_url":"https://www.graphcanon.com/categories/developer-tools.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/developer-tools"},{"slug":"llm-frameworks","name":"LLM Frameworks","url":"https://www.graphcanon.com/categories/llm-frameworks","markdown_url":"https://www.graphcanon.com/categories/llm-frameworks.md","api_url":"https://www.graphcanon.com/api/graphcanon/categories/llm-frameworks"}],"tags":[{"slug":"autoformalization","name":"autoformalization"},{"slug":"euclidean-geometry","name":"euclidean-geometry"},{"slug":"formalization","name":"formalization"},{"slug":"lean","name":"lean"},{"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-07-11T12:02:35.948Z","maintenance":{"label":"Slowing","score":36,"methodology":"github_public_v1","releases_90d":0,"days_since_push":227,"last_release_at":null},"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-07-11T12:02:39.221Z"},"deploy":{"source":"dockerfile:Dockerfile","self_host":true,"observed_at":"2026-07-11T12:02:39.221Z","managed_saas":false},"languages":{"value":["lean"],"source":"github.language","observed_at":"2026-07-11T12:02:39.221Z"},"has_docker":{"value":true,"source":"dockerfile:Dockerfile","observed_at":"2026-07-11T12:02:39.221Z"},"license_spdx":{"value":"MIT","source":"github.license","observed_at":"2026-07-11T12:02:39.221Z"}}}}