OpenSkillIndex← back to search
claude-codescience

Babysitter lean-proof-assistant

Interface with Lean 4 proof assistant for formal theorem verification

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/mathematics/skills/lean-proof-assistant" ~/.claude/skills/a5c-ai-babysitter-lean-proof-assistant && rm -rf "$T"
manifest: library/specializations/domains/science/mathematics/skills/lean-proof-assistant/SKILL.md
tags
#theorem-proving#mathematics#formal-verification#lean-4#mathlib4
source content

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