lean4-theorem-proving
AdvisoryAudited by Static analysis on Apr 30, 2026.
Overview
No suspicious patterns detected.
Findings (0)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
A repair run could change proof files or other files in the working tree.
The documented repair workflow applies patches and rebuilds Lean files. This is aligned with the theorem-proving purpose, but it can modify user source files.
git apply patch.diff lake build FILE.lean
Run it on a git branch or clean working tree, use the interactive repair mode when possible, and review diffs before committing.
If you run referenced scripts from another location, their behavior depends on that external installation rather than this reviewed instruction-only package.
The skill references helper scripts and command documentation that are not included in the provided manifest, so those helpers could not be reviewed here.
Automation Scripts | 19 tools for search, verification, refactoring, repair | Plugin `scripts/` directory
Only run referenced helper scripts from a trusted, reviewed installation, and verify their paths before execution.
Private Lean code or compiler output may be processed by delegated model workflows during repair.
The repair process may delegate proof context to another agent/model. This is disclosed and bounded, but users should be aware that local code and compiler errors may be included in that context.
If solvers fail → call `lean4-proof-repair` agent ... Stage 1: Haiku ... Stage 2: Sonnet ... max 24 attempts
Avoid running automated repair on files containing secrets, and use confirmation-based workflows for sensitive projects.