skills.rest
cameronfreer
cameronfreerCOMMUNITY
Explore all skills by this author →
WebsiteGitHub

lean4-theorem-proving

Automates Lean 4 theorem-proving tasks by diagnosing and repairing proofs, including sorries and axiom management.

360|43|Updated Oct 17, 2025
Search Tags:#proof automation#formal verification#mathlib#theorem proving#lean 4#mathematics#type classes
One-click install
npx skills add https://github.com/cameronfreer/lean4-skills --skill lean4-theorem-proving
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: lean4-theorem-proving
Source: https://github.com/cameronfreer/lean4-skills/tree/main/lean4-theorem-proving
Command: npx skills add https://github.com/cameronfreer/lean4-skills --skill lean4-theorem-proving

SYSTEM DOCUMENTATION & REQUIREMENTS

💡 This Skill requires ripgrep, curl, jq, python3, lean4, and includes scripts (resource) and references (resource) components.

What problem does it solve?

Lean 4 proof development is notoriously complex, time-consuming, and prone to errors, especially when dealing with type class inference, axiom management, and navigating the vast Mathlib. This Skill empowers you to overcome these challenges by providing battle-tested workflows, automation tools, and expert guidance, ensuring your formal proofs are correct and complete.

Core Features & Use Cases

  • Systematic 4-Phase Workflow: Structure proofs before solving, build helper lemmas bottom-up, fill sorries incrementally, and manage type class instances effectively.
  • 16 Automation Scripts: Leverage tools for searching Mathlib, analyzing proof complexity, tracking incomplete proofs (sorry statements), verifying axiom usage, and minimizing imports.
  • Comprehensive Reference Guides: Access in-depth documentation on essential tactics, Mathlib integration, common compilation errors, and domain-specific patterns for measure theory, probability, and algebra.
  • Use Case: Automate the formalization of complex mathematical theorems, contribute to Mathlib, or debug persistent "failed to synthesize instance" errors, all while ensuring your proofs are axiom-free and fully verified.

Quick Start

Example: Get a quick report on all incomplete proofs (sorries)

scripts/sorry_analyzer.py src/ --format=markdown > SORRIES.md

Frequently Asked Questions about lean4-theorem-proving

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I fix failed type class synthesis errors in Lean 4 proofs?▼

Type class synthesis errors occur when Lean cannot automatically infer instances. This Skill diagnoses these failures and repairs them using haveI/letI instance management, Mathlib search integration, and domain-specific tactics to resolve inference bottlenecks systematically.

What's the best way to find and eliminate sorry statements from Lean 4 theorems?▼

Track incomplete proofs using the sorry_analyzer.py script to generate reports on all unfinished proof steps. The Skill automates incremental repair workflows and helps replace sorries with verified tactics, ensuring proofs are complete and axiom-free.

Can I automate Mathlib searching and theorem discovery in Lean 4?▼

Yes. This Skill integrates Mathlib search into your proof workflow through automation scripts that locate relevant lemmas and theorems, reducing manual navigation time and surfacing helper results for faster formalization across pure math, measure theory, and probability domains.

How do I structure and debug complex Lean 4 proofs systematically?▼

The Skill provides a 4-phase workflow: structure proofs before solving, build helper lemmas bottom-up, fill sorries incrementally, and manage type class instances. Automation scripts analyze proof complexity and track axiom usage to ensure correctness.

What does the build-first workflow mean for Lean 4 theorem proving?▼

Build-first prioritizes compilation before completing logic, catching type errors early. This Skill guides you through constructing helper lemmas incrementally and verifying intermediate steps, reducing costly debugging cycles in formal verification and mathematical formalization.

Can I use this for program verification and measure theory proofs?▼

Yes. The Skill covers domain-specific tactics for pure math, measure theory, probability, and program verification. It provides reference guides and patterns tailored to each domain, ensuring tactics and instance management fit your formal verification context.

Related Skills

Explore More Education & Research Skills→
AribSudiaAribSudia
2

arib-graph

Generate a JSON import graph of monorepo file dependencies using ripgrep.

Community
Intermediate
jeffrey-dot-lijeffrey-dot-li
2

draft

Generate Lean theorem and lemma skeletons with placeholder proofs.

Community
Intermediate
fmhallfmhall
1

lean-no-mathlib

Provide Lean 4 tactic alternatives for proofs without Mathlib.

Community
Advanced
ArabelaTsoArabelaTso
142

counterexample-debugger

Analyze Nitpick and QuickChick counterexamples to identify proof failure root causes.

Community
Intermediate