lean4

Name: lean4
Author: cameronfreer

186installs40forks

How to install lean4?

cameronfreer/lean4-skills/lean4

$npx -y skills add cameronfreer/lean4-skills --skill lean4

Installs into the current project.

Summary

Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, finding a counterexample to, refuting, or disproving a Lean statement, or

Files · 1

View on GitHub

SKILL.md

1	# Lean 4 Theorem Proving
2
3	Use this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.
4
5	## Core Principles
6
7	Search before prove. Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.
8
9	Build incrementally. Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.
10
11	Respect scope. Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.
12
13	Use 100-character line width for Lean files. Do not wrap lines at 80 characters — Lean and mathlib convention is 100. If a line fits within 100 characters, keep it on one line. See [mathlib-style](references/mathlib-style.md) for breaking strategies when lines exceed 100.
14
15	Mathlib style quick check. For ordinary mathematical lambdas, write `fun x ↦ ...` (`\mapsto`), not `fun x => ...`. Use `=>` for `match`/`do` branches and metaprogramming callback idioms. Prefer `show P by tac` for tactic proofs; use `show P from term` only for term proofs. See [mathlib-style](references/mathlib-style.md).
16
17	Preserve statements, signatures, and docstrings — they're the file's API. Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user explicitly requests changes; changing them can break callers or alter the theorem being proved. Inline comments may be adjusted, but docstrings may not. If a proof seems to require changing a statement or adding a custom axiom, stop and discuss first because that changes the contract or the proof's trust basis. Exception: within synthesis wrappers (`/lean4:formalize`, `/lean4:autoformalize`), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.
18
19	## Commands
20
21	\| Command \| Purpose \|
22	\|---------\|---------\|
23	\| `/lean4:draft` \| Draft Lean declaration skeletons from informal claims \|
24	\| `/lean4:formalize` \| Interactive formalization — drafting plus guided proving \|
25	\| `/lean4:autoformalize` \| Autonomous end-to-end formalization from informal sources \|
26	\| `/lean4:prove` \| Guided cycle-by-cycle theorem proving with explicit checkpoints \|
27	\| `/lean4:autoprove` \| Autonomous multi-cycle theorem proving with explicit stop budgets \|
28	\| `/lean4:disprove` \| Guided counterexample search with certified refutation \|
29	\| `/lean4:checkpoint` \| Save progress with a safe commit checkpoint \|
30	\| `/lean4:review` \| Read-only code review of Lean proofs \|
31	\| `/lean4:refactor` \| Leverage mathlib, extract helpers, simplify proof strategies \|
32	\| `/lean4:golf` \| Improve Lean proofs for directness, clarity, performance, and brevity \|
33	\| `/lean4:learn` \| Interactive teaching and mathlib exploration \|
34	\| `/lean4:doctor` \| Diagnostics, cleanup, and migration help \|
35
36	`/lean4:*` names are the native plugin's command aliases and also serve
37	as stable workflow names throughout this documentation. On hosts
38	without command registration (skill-only or portable installs), invoke
39	the `lean4` skill with your host's normal syntax and ask for the named
40	workflow — e.g., "Use the guided `prove` workflow on `Foo.lean:42`."
41
42	This plugin ships a host-agnostic parser (`lib/command_args/`) that covers the
43	parser-decidable startup rules of the seven parameter-heavy commands (`draft`,
44	`learn`, `formalize`, `autoformalize`, `prove`, `autoprove`, `disprove`). A small set of
45	documented startup rules in these commands depend on runtime context (repo-
46	level search, interactive prompting) and are applied by the command after
47	reading the parser's output. The other commands (`checkpoint`, `review`,
48	`refactor`, `golf`, `doctor`) remain model-parsed.
49	When a host adapter installs the `UserPromptSubmit` hook, the parser runs
50	before the model sees a `/lean4:*` prompt matching one of the seven covered
51	commands, injects a `validated-invocation` block into context, and rejects
52	invalid invocations at the hook level; invocations of the other commands pass
53	through unchanged. Hosts without the hook fall back to model-parsed startup
54	via the shared [command-invocation.md](references/command-invocation.md)
55	contract.
56	Commands always announce resolved inputs, reject invalid startup configs before
57	doing work, and treat wall-clock budg

People who liked this also viewed

6 picks

Type

lean4

186installs40forks

View on GitHub

How to install lean4?

cameronfreer/lean4-skills/lean4

$npx -y skills add cameronfreer/lean4-skills --skill lean4

Installs into the current project.

Summary

Files · 1

View on GitHub

SKILL.md

1	# Lean 4 Theorem Proving
2
3	Use this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.
4
5	## Core Principles
6
7	Search before prove. Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.
8
9	Build incrementally. Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.
10
11	Respect scope. Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.
12
13	Use 100-character line width for Lean files. Do not wrap lines at 80 characters — Lean and mathlib convention is 100. If a line fits within 100 characters, keep it on one line. See [mathlib-style](references/mathlib-style.md) for breaking strategies when lines exceed 100.
14
15	Mathlib style quick check. For ordinary mathematical lambdas, write `fun x ↦ ...` (`\mapsto`), not `fun x => ...`. Use `=>` for `match`/`do` branches and metaprogramming callback idioms. Prefer `show P by tac` for tactic proofs; use `show P from term` only for term proofs. See [mathlib-style](references/mathlib-style.md).
16
17	Preserve statements, signatures, and docstrings — they're the file's API. Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user explicitly requests changes; changing them can break callers or alter the theorem being proved. Inline comments may be adjusted, but docstrings may not. If a proof seems to require changing a statement or adding a custom axiom, stop and discuss first because that changes the contract or the proof's trust basis. Exception: within synthesis wrappers (`/lean4:formalize`, `/lean4:autoformalize`), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.
18
19	## Commands
20
21	\| Command \| Purpose \|
22	\|---------\|---------\|
23	\| `/lean4:draft` \| Draft Lean declaration skeletons from informal claims \|
24	\| `/lean4:formalize` \| Interactive formalization — drafting plus guided proving \|
25	\| `/lean4:autoformalize` \| Autonomous end-to-end formalization from informal sources \|
26	\| `/lean4:prove` \| Guided cycle-by-cycle theorem proving with explicit checkpoints \|
27	\| `/lean4:autoprove` \| Autonomous multi-cycle theorem proving with explicit stop budgets \|
28	\| `/lean4:disprove` \| Guided counterexample search with certified refutation \|
29	\| `/lean4:checkpoint` \| Save progress with a safe commit checkpoint \|
30	\| `/lean4:review` \| Read-only code review of Lean proofs \|
31	\| `/lean4:refactor` \| Leverage mathlib, extract helpers, simplify proof strategies \|
32	\| `/lean4:golf` \| Improve Lean proofs for directness, clarity, performance, and brevity \|
33	\| `/lean4:learn` \| Interactive teaching and mathlib exploration \|
34	\| `/lean4:doctor` \| Diagnostics, cleanup, and migration help \|
35
36	`/lean4:*` names are the native plugin's command aliases and also serve
37	as stable workflow names throughout this documentation. On hosts
38	without command registration (skill-only or portable installs), invoke
39	the `lean4` skill with your host's normal syntax and ask for the named
40	workflow — e.g., "Use the guided `prove` workflow on `Foo.lean:42`."
41
42	This plugin ships a host-agnostic parser (`lib/command_args/`) that covers the
43	parser-decidable startup rules of the seven parameter-heavy commands (`draft`,
44	`learn`, `formalize`, `autoformalize`, `prove`, `autoprove`, `disprove`). A small set of
45	documented startup rules in these commands depend on runtime context (repo-
46	level search, interactive prompting) and are applied by the command after
47	reading the parser's output. The other commands (`checkpoint`, `review`,
48	`refactor`, `golf`, `doctor`) remain model-parsed.
49	When a host adapter installs the `UserPromptSubmit` hook, the parser runs
50	before the model sees a `/lean4:*` prompt matching one of the seven covered
51	commands, injects a `validated-invocation` block into context, and rejects
52	invalid invocations at the hook level; invocations of the other commands pass
53	through unchanged. Hosts without the hook fall back to model-parsed startup
54	via the shared [command-invocation.md](references/command-invocation.md)
55	contract.
56	Commands always announce resolved inputs, reject invalid startup configs before
57	doing work, and treat wall-clock budg

People who liked this also viewed

6 picks

Type