skills.rest
trailofbits
trailofbitsOFFICIAL
Explore all skills by this author →
Website𝕏@trailofbitsGitHub

writing-lean-proofs

Writes and reviews structured Lean 4 proofs following Mathlib conventions.

6.9k|598|Updated Jan 14, 2026
Search Tags:#formal verification#mathlib#theorem proving#proof writing#linters#tactics#Lean 4
One-click install
npx skills add https://github.com/trailofbits/skills --skill writing-lean-proofs
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: writing-lean-proofs
Source: https://github.com/trailofbits/skills/tree/main/plugins/writing-lean-proofs/skills/writing-lean-proofs
Command: npx skills add https://github.com/trailofbits/skills --skill writing-lean-proofs

SYSTEM DOCUMENTATION & REQUIREMENTS

💡 This Skill includes references (resource) components.

What problem does it solve?

Lean 4 proofs that merely compile are often fragile, unreadable, and impossible to maintain across Mathlib upgrades. This Skill provides a complete methodology for designing definitions and theorem statements first, building compiling sorry skeletons, and filling proofs with structured, linter-verified tactics.

Core Features & Use Cases

  • Top-down design workflow: Design definitions and their API lemmas (ext, simp, coercion, injectivity) before proving anything, using sorry skeletons that compile so work can be parallelized across contributors or agents.
  • Structured proof style: Enforces calc blocks, focused goal dots, honest show statements, have/suffices skeletons, and correct simp discipline (unsqueezed terminal simp, squeezed non-terminal simp).
  • Mechanical verification: Gates unproved obligations via Lean.collectAxioms instead of grep, configures project-appropriate linter profiles in CI, and guides writing custom @[env_linter] checks for project-specific conventions.
  • Use Case: A team formalizing a cryptographic protocol in Lean 4 uses this Skill to state all theorems as compiling sorry stubs, assign stubs to individual contributors, and enforce a CI gate that fails on any sorryAx or unexpected axiom.

Quick Start

Ask the assistant to help write or review a Lean 4 proof using Mathlib conventions, starting from a compiling sorry skeleton of the target theorem.

Frequently Asked Questions about writing-lean-proofs

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

FAQPage Schema
How do I structure a long Lean 4 tactic proof?▼

Start with a sorry skeleton using have, suffices, and calc so the structure compiles, then fill each step. Focus every subgoal with a dot block, open blocks with an honest show statement, and extract repeated or independently interesting fragments into lemmas.

How do I check a Lean project for remaining sorry placeholders?▼

Use Lean.collectAxioms or #print axioms rather than grepping for the word sorry. Grep matches comments and misses theorems that apply unproved helpers, while axiom collection catches exactly the real unproved obligations and unexpected trust assumptions like native_decide.

Should I enable linter.mathlibStandardSet in my own Lean project?▼

No, the full Mathlib standard set mixes proof-robustness checks with Mathlib-specific repository policy. Choose individual options by project role: a self-contained proof needs multiGoal, setOption, show, and auxLemma, while a reusable library adds flexible, missingEnd, and the unused-instance checks.

Why does my simp lemma never fire in Lean 4?▼

Common causes are numeral spelling mismatches (2^32 versus 4294967296), side conditions chained deeper than the default maxDischargeDepth of 2, and traversal order rewriting away the pattern first. Prefer structural LHS patterns and raise maxDischargeDepth for chained conditional rewrites.

When should I not use this Lean proof methodology?▼

It does not apply to Lean 4 used as a general-purpose programming language without proofs, to Coq, Isabelle, Agda, or Lean 3 where conventions differ, or to verified-software projects with their own house style that overrides Mathlib defaults.

Related Skills

Explore More Software Engineering Skills→
flonatflonat
127

lean-check

Formalize mathematical statements in Lean 4 and verify them with lake build.

Community
Advanced
AMGrobelnikAMGrobelnik
1

lean

Compile and verify Lean 4 code with Mathlib integration.

Community
Intermediate
santosomarsantosomar
1

nl-to-constraints

Translate natural-language requirements into formal constraints and property-based tests.

Community
Intermediate
dzackgarzadzackgarza
1

theorem-proving-and-counterexamples

Formalize and verify mathematical problems using ITPs and SMT solvers.

Community
Advanced