# Lean Proof Assistant

> Interface with Lean 4 proof assistant for formal theorem verification

- Skill: `majiayu000/lean-proof-assistant` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add majiayu000/lean-proof-assistant`
- Raw SKILL.md: https://api.skillmd.com/api/skills/majiayu000/lean-proof-assistant/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: majiayu000 (https://skillmd.com/u/majiayu000)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/majiayu000/lean-proof-assistant

---


# Lean Proof Assistant

## Purpose

Provides expert guidance on using the Lean 4 proof assistant for formal theorem verification and mathematical formalization.

## Capabilities

- Parse informal proofs into Lean 4 syntax
- Generate tactic-based proof scripts
- Access Mathlib4 library for standard results
- Automated term rewriting and simplification
- Generate proof outlines with sorry placeholders
- Extract executable code from proofs

## Usage Guidelines

1. **Proof Development**: Use Lean 4 syntax with Mathlib4 conventions
2. **Tactic Application**: Apply tactics systematically (intro, apply, exact, rw)
3. **Library Navigation**: Search Mathlib4 for existing lemmas and theorems
4. **Proof Completion**: Fill sorry placeholders incrementally

## Tools/Libraries

- Lean 4
- Mathlib4
- Lake build system
- VS Code Lean extension