AgentSkillsCN

lean4-proofs

Lean 4中的定理证明指南，包括项目搭建与证明规范。

SKILL.md
--- frontmatter
name: lean4-proofs
description: Guidelines for theorem proving in Lean 4, including project setup and proof conventions.

Lean 4 Proofs

Setup

bash
lake init MyProject
lake build

Structure

code
lean/
├── lakefile.lean
├── lean-toolchain
├── Main.lean
└── MyProject/

Naming

  • •Types: PascalCase
  • •Terms/theorems: camelCase
  • •Namespaces: PascalCase

Tactics

lean
-- Basic: intro, apply, exact, rfl, simp, ring
-- Structural: have, let, show, calc
-- Case analysis: cases, induction, rcases
-- Finishing: trivial, contradiction, omega

Best Practices

  • •Start with sorry placeholders
  • •Build incrementally with lake build
  • •Leverage Mathlib when appropriate