본문으로 건너뛰기
cccskills
무료GitHub에 공개

math-formalization

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。

tradecatlabs/vibe-coding-cn
설치 방법 보기

이럴 때 유용합니다

  • Verifying an important lemma with Lean 4
  • Breaking a theorem into definitions and supporting lemmas
  • Checking proofs for sorry, admit, and unauthorized axioms
  • Reviewing whether a formal statement matches the original claim

포함된 파일(6)

  • SKILL.md4.6 KB
  • CHANGELOG.md757 B
  • references/index.md142 B
  • references/pressure-tests.md2.4 KB
  • references/source-map.md1.4 KB
  • VERSION6 B

SKILL.md(원문)

설치하기 전에 에이전트에게 전달되는 지시 내용을 확인할 수 있습니다.

Math Formalization

把数学主张转成可由 proof assistant 内核检查的最小切片；当前环境缺工具时只产出计划，不伪造验证。

Position in the Method Map

Lean 是形式化方法中的依赖类型理论型交互式定理证明平台，主战场属于“演绎验证 / 定理证明”，不是形式化方法的同义词。先用 governance/standards/FORMAL-METHODS-MAP.md 固定规格与语义，再进行 Lean 语言/elaboration、proof engineering、自动化、Mathlib library engineering 和应用形式化。simp、grind、SMT 或符号执行可以辅助找证明，但最终的 kernel 检查和 statement-faithfulness 审查必须分开记录。

When to Use This Skill

  • 用户明确要求 Lean 4、Mathlib 或机器检查证明。
  • 自然语言证明已经稳定，需要验证关键引理或高风险步骤。
  • 需要建立 definitions/imports/lemmas/theorem 的形式化依赖结构。

Not For / Boundaries

  • CandidateObservation 或 formal-conjectures 条目只有在明确用户形式化请求或 active ProblemContract 下才能进入形式化；benchmark statement/build 不创建数学 Result。
  • formal-conjectures 只使用 vendor lock 固定 commit/immutable benchmark snapshot；其上游也明确要求人工审查 misformalization，固定或编译成功不替代 statement faithfulness。
  • 每次任务开始时运行时探测 lean、elan 和 lake；所需工具缺失时才 fail-closed 为 calibration/blocked，不得把主机安装状态缓存为 skill 事实。
  • 含 sorry、admit、未授权 axiom 或编译失败的文件不得标记 kernel-checked。
  • 不采用归档 skill 中未经验证的 lean_agent Python API。
  • 形式化成功证明 Lean 陈述成立，不自动证明它忠实表达原自然语言命题；必须做 faithfulness audit。
  • verified=false、timeout、unsupported、编译错误和基础设施错误都不是数学反例；必须保留失败类别。
  • 调用者自报的 verified、历史 PASS 或只存在的 receipt 文件没有通过权；证据必须绑定当前输入、工具链和真实产物。

Quick Reference

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。

Examples

Example 1：工具缺失

  • 输入：“把这个引理用 Lean 验证。”
  • 动作：运行预检，发现 lean 缺失；输出安装前置和形式化切片。
  • 验收：状态是 blocked，不创建伪编译日志。

Example 2：含 sorry

  • 输入：一个能够编译但包含 sorry 的 Lean 文件。
  • 动作：扫描占位符并阻止通过。
  • 验收：不能标记 kernel-checked，报告具体文件/位置。

Example 3：陈述失真

  • 输入：Lean 证明了比原命题更弱的结论。
  • 动作：proof check 与 faithfulness audit 分开裁决。
  • 验收：内核检查可 PASS，但总体状态仍因表达不忠实而 BLOCK。

Example 4：验证超时

  • 输入：proof assistant adapter 超时并返回 verified=false。
  • 动作：记录 timeout、预算、工具链和未闭合义务。
  • 验收：状态为 blocked/timeout，不把原命题标记 refuted。

References

  • references/source-map.md：Lean Skill、receipt、adapter 与 faithfulness checker 的来源和限制。
  • references/pressure-tests.md：占位证明、证据新鲜度、claim strength、失败分类与陈述忠实性压力场景。

Maintenance

  • Sources：wentor-research-plugins、leanprover-skills、mathevidence、itpeval、atp-checkers；只吸收方法、不变量和反例，不直接激活上游代码。
  • Last updated：2026-08-26。
  • Verification：安装后必须用当前 Lean/Mathlib 官方工具运行最小无 sorry vertical slice。

리뷰

아직 리뷰가 없습니다. 사용해 본 소감을 남겨 주세요.

댓글

로그인 없이 쓸 수 있습니다. 사용 후기, 질문, 작동하지 않은 환경 등을 편하게 남겨 주세요.

아직 댓글이 없습니다. 첫 댓글을 남겨 보세요.

보내면 바로 공개됩니다. 이메일 주소나 전화번호 같은 개인 정보는 쓰지 마세요. URL은 2개까지입니다.

0 / 1,000자

이 양식은 reCAPTCHA로 보호되며 Google 개인정보처리방침 및 서비스 약관이 적용됩니다.

같은 저장소의 스킬

analyzing-ethereum-smart-contract-vulnerabilities

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Checking Solidity contracts before deployment
  • Investigating reentrancy and access control weaknesses
  • Consolidating findings from Slither and Mythril
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

auditing-foundry-smart-contract-security

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Auditing Solidity contracts before deployment
  • Adding fuzz and invariant tests for contracts that move funds
  • Reviewing private key storage and deployment scripts
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

auto-skill

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Creating a skill from documentation, code, or specifications
  • Reorganizing an overly long SKILL.md
  • Clarifying when a skill should activate
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

auto-tmux

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Inspect output and errors across multiple AI terminals
  • Resume tasks waiting for confirmation
  • Coordinate tasks and file locks across AI workers
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

math-computation

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Checking identities and integrals with exact arithmetic
  • Searching a defined range for counterexamples
  • Cross-checking numerical results at higher precision
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

math-derivation

무료

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.

한국어 요약은 준비 중입니다. 영어 요약을 표시하고 있습니다.

  • Organize scattered formulas and theory notes
  • Trace the steps behind an algebraic identity
  • State conditions and error orders for approximations
tradecatlabs/vibe-coding-cn1.8만2026년 10월 19일 업데이트

tradecatlabs의 스킬 모두 보기

이 스킬의 문제 신고