Menu

Individual skill

writing-lean-proofs

Use when asked to design, write, review, refactor, lint, or performance-diagnose Lean 4 proofs, libraries, or tactics. Not for non-Lean code or changes outside source, API, proof, or linter scope.

.devin/skills/writing-lean-proofs/SKILL.md

Read pinned source

Source commit b0e8ce89a19fac880251dc3ea1babfeb4503a4fe

What was checked

Matches the observed repository HEAD
Yes
Scanner rules are current
Yes
Repository scan complete
No
Skill scan complete
No
Observed behavior
Instructions only
Last checked
Nov 4, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings)
55
Repository last updated
Sep 28, 2026
License
Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files
Read excerpt

# Writing Lean proofs

## Contract

| Field | Bound contract |
|---|---|
| Trigger | The task is to design, write, review, refactor, lint, or performance-diagnose Lean 4 proofs, libraries, or tactic extensions under Mathlib conventions. |
| Authority | Reversible local: writes only Lean source files, library API, proof structure, and project linter configuration, plus scoped mechanical Lean checks; rollback is version control. No remote mutation. |
| Side effect | Local writes to Lean source, library API, proof structure, project linter configuration, and scoped mechanical Lean checks. No remote mutation, credential change, paid action, or deployment. |
| Done | The requested Lean declarations have stable statements and structured proofs, compile under the project toolchain, and satisfy the selected axiom and linter policy. |

## Inputs

A Lean 4 project with a working `lakefile.lean` and toolchain (`lean-toolchain`) is required, along with target theorem statements, definitions to formalize, or proof obligations to discharge. Optional inputs include project-specific linter configuration, axiom policy (default: `[propext, Classical.choice, Quot.sound]`), `maxHeartbeats` budget, and Mathlib dependency.