Formalize Math Paper — Security skill for Claude Code

formalize-math-paper

An [Agent Skill](https://agentskills.io) for formalizing a mathematics research paper in Lean 4 with Mathlib, in any field of mathematics. It works with any agent that supports the `SKILL.md` format: Claude Code, OpenAI Codex, Gemini CLI, Google Antigravity, GitHub Copilot, Cursor, OpenCode, Amp and others.

The skill guides the work end to end:

• read the paper and record its results, constants, citations and suspected typos;
• set up a Lean project on current Mathlib, using the module system;
• state every result first, and check each statement against the paper's TeX source;
• prove everything the paper proves (Stage 1), then every result it cites (Stage 2), until the project has no sorry and no axiom;
• verify: the axioms of every declaration, and Comparator;
• clean up: remove unused hypotheses and other warnings;
• write REPORT.md, an audit of the paper against the formalization (errors and gaps, missing and redundant hypotheses, how the paper uses each cited result), and README.md;
• package the project for the Palomar registry (Challenge/Solution, comparator.json, formalization.yaml, preflight).

It also covers turning an existing, never-compiled Lean draft into a project that builds.

Install

With the [`skills`](https://github.com/vercel-labs/skills) installer, which detects your agents and links the skill into each of them:

npx skills add vltanh/formalize-math-paper -g      # for your user; omit -g to install into the current project

The installer puts the skill in `~/.agents/skills/`, which most agents read, and links it into the directories of those that do not. Antigravity reads user-wide skills only from `~/.gemini/config/skills/`, so link it there too:

mkdir -p ~/.gemini/config/skills && ln -s ~/.agents/skills/formalize-math-paper ~/.gemini/config/skills/

Or copy the repository into your agent's skills directory by hand:

git clone https://gith