Individual skill

lean4-mathlib

Formalizes and checks mathematical statements in Lean 4 with Mathlib, covering the lake project layout and pinned toolchain, `lake exe cache get` before `lake build`, searching Mathlib through Loogle, `exact?`, `apply?` and `simp?`, tactic hygiene, finishing without `sorry`, auditing with `#print axioms`, and making sure the formal theorem statement matches the informal claim exactly. Use when asked to prove, formalize, check or repair a Lean theorem or a Mathlib-based development; use the coq skill for Coq or Rocq, and ordinary mathematical writing for informal proofs.

backend/cli/skills/other/lean4-mathlib/SKILL.md

Read pinned source

Source commit a08e0ad0ad3d6448123039ee4659163eb2e35d99

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: Yes
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Network or broad shell
Last checked: Nov 2, 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): 4,352
Repository last updated: Nov 6, 2026
License: Apache-2.0

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

agent Repository topic
ai Repository topic
bun Repository topic
cli Repository topic
llm Repository topic
ml Repository topic
open-source Repository topic
research Repository topic
science Repository topic
ai-agent Repository topic
writing Derived category

Files and excerpt

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

Browse files

SKILL.mdcore · 6,309 bytes

Read excerpt


# Lean 4 and Mathlib

A Lean proof is only as good as its statement. `sorry` compiles; a theorem about the wrong
object compiles; a theorem with an unsatisfiable hypothesis compiles. The work is statement
fidelity first, search before proving, build, then audit the axioms.

## Project layout

1. A Mathlib-dependent project has `lakefile.lean` or `lakefile.toml` (with
   `require mathlib from git "https://github.com/leanprover-community/mathlib4"`),
   `lean-toolchain` (the exact Lean version; it must match Mathlib's own `lean-toolchain`
   or the cache will not apply), and `lake-manifest.json` (locked dependency revisions).
   `lake new <name> math` scaffolds this. Do not run `lake update` casually: it moves the
   Mathlib revision and forces a full rebuild.