ziwaa-se

Kappa — Development skill for Claude Code

Development community

KAPPA: Kit of Agents for Proof-checking Papers with a proof Assistant.

How to install Kappa

This entry records only its repository, not the path inside it, so there is no exact command to give. Open ziwaa-se/kappa and copy the folder into ~/.claude/skills/, or the file into ~/.claude/agents/.

What Kappa does

KAPPA: Kit of Agents for Proof-checking Papers with a proof Assistant. Checks the proofs in LaTeX papers with Lean 4 and Claude Code agents.

Alternatives in Development

Lean Canvas — Generate Lean Canvas with problem, solution, UVP, and metrics 7.8k ★
Claude Prism — An offline-first scientific writing workspace powered by Claude 1.1k ★
Kaizen — Applies continuous improvement methodology with multiple analytical approaches, based on Japanese Kaizen philo 663 ★

README

KAPPA

*Kit of Agents for Proof-checking Papers with a proof Assistant*, released as the TeX Proof-Check Kit up to v1.3.4.

Paper: [arXiv:2610.35596](https://arxiv.org/abs/2610.35596) · [How to cite](#citing-kappa)

**Check the proofs already written in a LaTeX paper by translating them faithfully into Lean 4**, with a team of [Claude Code](https://code.claude.com/docs) agents that review each other's work. Every numbered result (theorem, proposition, lemma, corollary) gets one of four verdicts:

Verdict	Meaning
Verified unconditionally	The paper's own proof compiles in Lean, with no unproved input
Verified conditionally	It compiles, but relies on results the paper cites or does not prove. These are explicit, named Lean hypotheses that a person should check
Issue recorded	A confirmed problem, located in the paper and classified by whose fault it is: false statement (`ERROR`), a justification that fails, a missing hypothesis, an uncovered case, an ambiguous domain
Unfinished	Stopped, with the reason recorded. Never counted as an error in the paper

**Scope of this version.** The kit **verifies proofs that are already written**. It checks the argument the authors wrote, step by step, and reports exactly where it holds and where it fails. It does **not** repair proofs, search for different proofs, or edit the paper. When it finds a problem, it records the evidence and the minimal change that would remove it; when the authors revise the paper, it re-checks the changed results. A mode that also proposes and verifies corrections is planned; see the [Roadmap](#roadmap).

Example

[`examples/full-workflow`](examples/full-workflow/) is a two-page note with three results, taken through the whole workflow: a first check, a corrected version of the paper, a condition checked by a person, and the final report. Real output of one run:

| Result | First check | After the authors' revision and a person's check