openmath-lean-theorem

• Analyzed: May 14, 2026, 7:41 AM
• Findings: 1
• Version: 1.0.3
• Hash: 44143712015ff27fba1e7bd1498baff1882ac9337c5fd9653655c5b80bb6cd3f
• Source: palm
• External report: View on VirusTotal

Findings (1)

The skill bundle provides a legitimate environment for proving Lean theorems, including a preflight script (scripts/check_theorem_env.py) that validates toolchains and manages dependencies. While the script includes a capability to clone a remote repository (https://github.com/leanprover/skills.git) and install additional skills, this behavior is explicitly documented in SKILL.md as a side effect, requires opt-in flags (--auto-install-skills), and enforces the use of an explicit installation directory to prevent unauthorized modifications. The code uses safe subprocess handling, includes safety checks for directory creation, and lacks any indicators of data exfiltration, persistence, or malicious intent.