agentmods.dev

lean-physics

lean-physics is a skill for Claude Code, Codex from xi-zhao/OpenQuantum. It costs 60 tokens per session (1,507 once invoked), scanned A, original, MIT.

A Lean 4 setup for formally checking mathematical and physics statements, including quantum-information and Pauli-matrix results. Lean is a programming language and proof checker; passing a formal proof does not prove that a physical model matches reality.

In plain words
What is it for?
Use it to write and check Lean proofs with mathlib and physlib, inspect dependencies, and prepare the required fixed toolchain.
Why use it?
It helps audit definitions, assumptions, theorem reuse, and formal derivations in a fixed software environment. It keeps formal verification separate from numerical results and scientific validation.

Skill for Claude CodeCodex

Written for no agent in particular: nothing here depends on one. Also seen: installed under .agents/ (shared by several agents).

not rated 71repo yesterday A scan 60 tokens original MIT

Good fit Use it to write and check Lean proofs with mathlib and physlib, inspect dependencies, and prepare the required fixed toolchain.

Compare 6 skills from other repositories ↓
Install with agentmods
npx agentmods add skills/xi-zhao/openquantum/lean-physics
View source ↗ xi-zhao/OpenQuantum xi-zhao.github.io
Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

Any agent
npx skills add xi-zhao/OpenQuantum --skill lean-physics
Clone the repo
git clone --depth 1 https://github.com/xi-zhao/OpenQuantum

Made for: Claude Code, Codex.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

agentmods badge for lean-physics

README.md
[![agentmods](https://agentmods.dev/badge/skills/xi-zhao/openquantum/lean-physics/github.svg)](https://agentmods.dev/skills/xi-zhao/openquantum/lean-physics)
Your own site
<a href="https://agentmods.dev/skills/xi-zhao/openquantum/lean-physics"><img src="https://agentmods.dev/badge/skills/xi-zhao/openquantum/lean-physics/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

agentmods 80×15 button for lean-physics

Your own site · 80×15
<a href="https://agentmods.dev/skills/xi-zhao/openquantum/lean-physics"><img src="https://agentmods.dev/badge/skills/xi-zhao/openquantum/lean-physics.svg" alt="Reviewed on agentmods" width="80" height="20"></a>
Per session 60 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.
When invoked 1,507 The whole file, excluding the scripts and references it only reads on demand.
Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe.
Origin original No closer match found in the catalogue.
Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

ModelPer sessionOnce invoked
Fable 5.1 $0.00060 $0.01507
Opus 5.5 $0.00024 $0.00603
Sonnet 5.5 $0.00012 $0.00301
Haiku 4.5 $0.00006 $0.00151

Measured 9d ago against content hash 6928f2fb25ed, method: parsed. Prices are Anthropic first-party input rates as of 2026-10-07, from the pricing page.

Security

Grade A, and why

lean-physics scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 9d ago.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

.agents/skills/lean-physics/SKILL.md · 70 lines

How it starts

The opening of the file, as written. The whole thing — 70 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Lean 数学与物理证明

原生 SDK 路径

本能力使用 Lean 4 / mathlib / physlib 的原生公开 API。用户需要 数学与物理命题、Pauli 矩阵关系、量子信息定理与依赖公理审计 时，由 Agent 在固定依赖环境中编写和运行任务代码。

使用 node scripts/sdk-access.mjs inspect lean-physics 定位环境，按完整 SDK 工作流执行。模块导航：Mathlib、Physlib、QuantumInfo；导航不是 API 白名单。

固定兼容的 Lean 4.35.0 与 Lake 依赖锁；显式准备导入闭包。形式证明仅覆盖给定定义和假设，不代表真实物理或科学验收。

本入口复用宿主文件与代码工具，没有新增通用执行 Tool。原生 SDK 受上游版本、可选依赖、宿主资源与用户授权约束。已禁用或被拒绝的动作不能借代码路径绕过。执行状态和科研验收分别报告。

选择与边界

当用户要检查形式推导、定义中的假设或复用已有定理时使用。本 Skill 复用宿主文件与代码工具， 没有专用证明 Tool 或 MCP Server。数值模拟继续使用对应量子 SDK；Lean 接受证明项不表示 形式定义符合真实物理系统，也不验证数值实现、硬件或科研结论。科学状态保持 not_evaluated。

固定环境与准备

使用 node scripts/sdk-access.mjs inspect lean-physics 只读定位环境。Lean/Lake 为 4.35.0， mathlib 为 56a005855ea17e0b0958f73ec801ae140b0a1679，physlib 为 6fd50cbcfafb503e4b96435e49bedb0e220f09e2，间接依赖见 Lake 锁。 三者作为兼容组升级；不能单独改工具链或取另一个提交的缓存。

显式准备前指定 OPENQUANTUM_LEAN_BIN 为该版本实际 Lean 可执行文件的绝对路径， OPENQUANTUM_LEAN_ENV_ROOT 为本任务环境目录；需要工具链时从官方 release 获取并核对摘要。 不修改全局 elan、编辑器或已有用户 Lean 项目。遵守宿主安装授权、资源预算与外置盘规则。 node scripts/setup-sdk.mjs lean-physics 下载固定源码、按示例的导入闭包获取 mathlib 缓存并构建 小型证明；源代码、构建及缓存均留在指定环境。预计需要数 GiB，先检查空间。 默认仅准备示例的导入闭包，不声称已编译全部 Mathlib、Physlib 或 QuantumInfo。

准备后重新 inspect；只使用返回的绝对 run.command 与 run.environment.LEAN_PATH 检查保存到 用户工作区的 .lean 文件。执行不经 elan/Lake 自动下载。缺少其他模块的编译产物时，先用同目录 工具链在 leanProject.directory 显式运行 lake exe cache get <module>、lake --no-cache build <module>， 保留相同依赖锁与本地缓存目录，再继续证明检查；模块导航不是功能白名单。 准备拒绝覆盖已有模板或依赖源码修改；版本变化请保留旧环境，指定新的环境根目录。

证明工作流

  1. 明确待证命题、定义域、单位/归一化、有限维或无限维等假设。先查固定版本源码中的定义和已有定理。 新物理假设若改变结论，向用户给出具体取舍；不要为让证明通过偷偷弱化目标。
  2. 把命题写为具名 theorem，先用小型独立命题检查导入和记号。优先直接复用已有定理与内核可检查证明。
  3. 在保存文件上运行 Lean，保留完整错误/警告。错误命题必须报错；退出码为零仍需检查 sorry 警告。
  4. 对每个交付定理运行 #print axioms <name>，检查包括间接依赖的 sorryAx、自定义公理、 Lean.ofReduceBool 等非内核计算信任边界。允许的 propext、Classical.choice、Quot.sound 也须如实列出。禁止以 sorry、admit 或新公理绕过目标后宣称证明完成。
  5. 保存源文件、原始目标/假设、命令、Lean版本、依赖完整 SHA、输出及公理列表。 分开报告环境准备、文件编译、目标证明与科学验收；额外公理或未闭合目标明确标为未完成。

Read the full file on GitHub · 70 lines

Files

What ships with it

4 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

  1. 9d ago First seen · 70 lines · 60 tokens per session scan A 6928f2fb25ed

Subscribe to this mod's changes

lean-physics is a skill published in the GitHub repository xi-zhao/OpenQuantum (71 stars, last pushed yesterday), licensed MIT. It adds 60 tokens to every session and 1,507 once invoked, about $0.0002 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-10-29.

Learning and teachingScientificagentic-aiai-agentdeepseekdeepseek-harnessmcp-servermodel-context-protocol
Related

lean-physics compared with skills from other repositories

lean-physics next to 6 skills from other repositories
ModTypeStarsLast pushLicenceScanTokensWorks with
lean-physicsxi-zhao/OpenQuantumSkill71yesterdayMITA60Claude Code, Codex
dsh-tui-guideccch1mneyyy/dsh-TUISkill7.0kyesterdayMITA41Claude Code, Codex
manim-explainer-animationcalesthio/generative-media-skillsSkill2313mo agoMITA80Claude Code, Codex
rhylthymerhylthyme/rhylthyme-mcpSkill02d agoApache-2.0A167Claude Code
ask-sonnerstvlynn/dsh.fishSkill25d agoMITA97Claude Code
kill-ai-slopstvlynn/dsh.fishSkill25d agoMITA249Claude Code
pick-ui-librarystvlynn/dsh.fishSkill25d agoMITA61Claude Code