# Math Formal Proof

> Develop formal mathematical proofs in proof assistants (Lean 4, Coq, Isabelle, Agda) with literate programming, tactic-driven construction, and verification.

- Skill: `quantumquirkxyz/math-formal-proof` (Agent Skill)
- Install (CLI): `npx skillmds@latest add quantumquirkxyz/math-formal-proof`
- Raw SKILL.md: https://api.skillmd.com/api/skills/quantumquirkxyz/math-formal-proof/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: quantumquirkxyz (https://skillmd.com/u/quantumquirkxyz)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/quantumquirkxyz/math-formal-proof

---


## Contract

- **Input:** mathematical statement to prove and target proof assistant.
- **Output:** verified source + Markdown narrative.
- **Side effects:** none.
- **Dependencies:** none.
- **Stop condition:** proof verified by the assistant's kernel.
- **Risk:** low.
- **Boundary:** produces verified proof artifacts; no new external system changes.

# Formal Proof Development

Build a **proof** in a proof assistant — Lean 4, Coq, Isabelle, Agda — that the assistant's kernel can verify, with a literate narrative for publication.

## When to use

- A proof needs machine-verifiable rigour.
- A paper's appendix should include a formal proof (increasing trust).
- The researcher is formalising a known result or building a library (e.g. `mathlib`).

## Process

### 1. Pick the assistant

- **Lean 4 + mathlib** — large library, active community, default for many.
- **Coq** — mature; MathComp library for combinatorics.
- **Isabelle / HOL** — strong for analysis, logic, and computer-science theorems.
- **Agda** — small, expressive, dependent types.

State the choice and why.

**Completion criterion:** assistant named; rationale stated.

### 2. Encode the statement

Translate the mathematical statement into the assistant's syntax:

- Use existing types (`ℕ`, `ℝ`, `Group`, `TopologicalSpace`).
- Match the statement's quantifier structure.
- State the theorem header with named variables and explicit hypotheses.

**Completion criterion:** theorem header compiles; types check.

### 3. Choose proof strategy

- **Library search** — `library_search` / `Search` / `find` for an existing lemma.
- **Tactic decomposition** — `intro`, `apply`, `cases`, `induction`, `simp`.
- **Manual proof** — explicit term construction (`exact`, `λ`).
- **Proof by reflection** — for decidable equalities.
- **Proof by automation** — `aesop`, `omega`, `nlinarith`, `field_simp`.

**Completion criterion:** strategy named.

### 4. Build and verify

Write the proof step by step. After each step:

- Run the assistant's checker (`lake build`, `coqc`, `isabelle build`).
- Replace `sorry` and `Admitted` with verified tactics.
- Record the verified proof's hash or kernel confirmation.

**Completion criterion:** proof fully verified (no `sorry`/`Admitted`).

### 5. Literate export

For a paper:

- Use `preprint` / Lean+LaTeX integration, or extract the proof as LaTeX with a translator.
- Annotate key tactics with comments explaining the mathematical intuition.
- Cite the formal proof in the paper ("Verified in Lean 4; see Appendix B").

**Completion criterion:** narrative + verified proof saved; cross-reference to paper present.

## Notes

- Pair with `math-pure-proofs` for informal reasoning.
- For paper inclusion, use a versioned Git tag of the formal proof.