skill
職業分類
説明
更新
lean-review-refactor-policy
ソフトウェア開発者
Policy for non-semantic refactors that keep math meaning unchanged while making Lean/Mathlib code easier to review and harder to break: minimal imports, scoped assumptions, localized `classical`, proof tidying, lint fixes, perf/typeclass risk control, and PR splitting.
2026-04-13
mathlib-usage
数学者
Mathlib usage principles (imports, search, existence checks, confirmation) for all `.lean` files in this repo.
2026-04-13
prover-interface
コンピュータ・情報研究科学者
I/O contract for proof/counterexample/stuck attempts and post-attempt new-problem proposals.
2026-04-13
lean-rule
数学者
Rules to apply this repo's Lean workflow (plan → skeleton → error-driven iteration → mathlib search → minimal diffs) consistently across all `.lean` files.
2026-04-02