Turn mathematical claims into definitions, lemmas, and proofs for Lean 4 and Mathlib. Check proofs with Lean’s trusted core, separately review whether the formal statement matches the original claim, and record verification evidence.
中文简介正在准备中。当前显示英语简介。
数学形式化与 proof-assistant 验证。用户要求 Lean 4/Mathlib、formal proof、kernel check、无 sorry 编译，或需要把自然语言定理切成可形式化定义和引理时使用。缺少 Lean 工具链时必须 fail-closed。
安装前可以查看交给 AI 代理的指令内容。
把数学主张转成可由 proof assistant 内核检查的最小切片；当前环境缺工具时只产出计划，不伪造验证。
Lean 是形式化方法中的依赖类型理论型交互式定理证明平台，主战场属于“演绎验证 / 定理证明”，不是形式化方法的同义词。先用 governance/standards/FORMAL-METHODS-MAP.md 固定规格与语义，再进行 Lean 语言/elaboration、proof engineering、自动化、Mathlib library engineering 和应用形式化。simp、grind、SMT 或符号执行可以辅助找证明，但最终的 kernel 检查和 statement-faithfulness 审查必须分开记录。
lean、elan 和 lake；所需工具缺失时才 fail-closed 为 calibration/blocked，不得把主机安装状态缓存为 skill 事实。sorry、admit、未授权 axiom 或编译失败的文件不得标记 kernel-checked。lean_agent Python API。verified=false、timeout、unsupported、编译错误和基础设施错误都不是数学反例；必须保留失败类别。verified、历史 PASS 或只存在的 receipt 文件没有通过权；证据必须绑定当前输入、工具链和真实产物。command -v lean
command -v lake
lean --version
lake env lean Path/To/File.lean
rg -n '\b(sorry|admit)\b' .
形式化包必须包含：原命题、Lean 陈述、定义映射、imports、证明义务、实际命令、退出码、Lean/Mathlib 版本、axiom/sorry 审计和 faithfulness 状态。
验证 receipt 至少记录：当前请求/输入 digest、形式化产物或 theorem digest、checker 与 toolchain、请求和实际建立的 claim strength、未闭合义务、assurance mode、结构化结果状态与错误类别。claimEstablished 不得强于真实证据，也不得强于 claimRequested。
只有命令真实返回成功、无占位证明且陈述忠实审计完成，才能写 kernel-checked。
lean 缺失；输出安装前置和形式化切片。sorry 的 Lean 文件。verified=false。references/source-map.md：Lean Skill、receipt、adapter 与 faithfulness checker 的来源和限制。references/pressure-tests.md：占位证明、证据新鲜度、claim strength、失败分类与陈述忠实性压力场景。wentor-research-plugins、leanprover-skills、mathevidence、itpeval、atp-checkers；只吸收方法、不变量和反例，不直接激活上游代码。sorry vertical slice。还没有评价。欢迎分享你的使用感受。
无需登录即可发表。欢迎分享使用感受、提问，或说明在哪些环境下无法运行。
还没有评论。来写第一条吧。
Analyze Solidity smart contracts with Slither and Mythril before Ethereum deployment. Combine code inspection with execution path analysis, review potential vulnerabilities, remove duplicate findings, and produce an audit report with severity ratings and suggested fixes.
中文简介正在准备中。当前显示英语简介。
Audit Solidity contracts in Foundry projects before deployment using code analysis, randomized tests, manual review, and private key checks. Produces a JSON report with findings, remediation, test coverage, and a pass or fail deployment decision.
中文简介正在准备中。当前显示英语简介。
Build reusable Claude Skills from documentation, APIs, code, and specifications. Organize instructions and reference files, define clear activation conditions, add reproducible examples, and check new or existing skills against a delivery checklist.
中文简介正在准备中。当前显示英语简介。
Automate tmux, a tool for managing multiple terminal workspaces, to inspect output, send commands, monitor stalled tasks, and record logs. Coordinate multiple AI terminals with task queues, file locks, status tracking, and handoff reports.
中文简介正在准备中。当前显示英语简介。
Check mathematical expressions, solve equations, and search bounded ranges for counterexamples using symbolic and numerical libraries. Record assumptions, commands, and results so calculations can be repeated, while keeping computational evidence distinct from general mathematical proof.
中文简介正在准备中。当前显示英语简介。
Turn scattered formulas and theory notes into a derivation that can be checked step by step. Keep definitions and assumptions consistent, distinguish exact identities from approximations, and make hidden conditions and limits explicit.
中文简介正在准备中。当前显示英语简介。