Lean Git リポジトリのトップレベル README ファイルです。 このディレクトリには、Lean 4 の数学ライブラリや関連プロジェクトが含まれています。 各ディレクトリ１つの Git リポジトリとして管理されています。
本リポジトリは、ソフトウェア製品というより Lean による定理証明・形式化研究の記録 を目的としている。 そのため、Git の履歴は「動作コードの変更履歴」ではなく、 定理がどのように構築・洗練されていったかという研究過程そのものを保存する。
以下に、本リポジトリで採用している Git 運用方針を示す。
- ブランチは 削除しない
- ブランチは 定理・補題・一般化の試行過程そのもの
mainブランチは 確定した成果（結果）をまとめた正史- 試行錯誤の詳細な履歴は feature ブランチ側に残す
- 履歴の圧縮（rebase / squash）は 原則として行わない
※必須事項：直接 main ブランチで作業しないこと
- 公開・参照用の安定版
- 定理や補題が「成立した結果」として整理された状態
- 細かい試行錯誤のコミット履歴は載せない
- ドキュメント（README / Note / 論文草稿等）から参照される対象
- 新しい定理・補題・一般化・証明方針の試行
- Lean の証明過程・失敗・修正の履歴をすべて残す
- 「なぜこの補題が必要になったか」「どこで詰まったか」を後から追跡可能
- ドキュメントと ブランチ名を対応付けて参照される研究資料
- feature ブランチは
mainにマージする- 目的：成果を正史に反映し、ドキュメントから参照可能にするため
- 条件：定理・補題が成立し（ビルドエラーなし）、ドキュメントで参照される状態になったとき
- 手段：Pull Request を用いること
- レビューは必須ではないが、可能な限り第三者の目を通すことが望ましい
- マージ後も ブランチは削除しない
mainには成果のみを反映し、詳細な作業履歴は feature ブランチ側に保持する- マージ方法は以下のいずれかを状況に応じて選択する：
- 通常のマージ（merge commit を残す）
- squash マージ（main 側の履歴を簡潔に保つ場合）
※ squash マージを用いた場合でも、 feature ブランチ自体は削除せず、研究過程の記録として保持する。
マージ後の feature ブランチは、先端コミットまたはタグにより状態を示す。
closed: 作業完了・参照用として保存fix: main 反映後に軽微な修正を行った履歴- （必要に応じて）
superseded: 後続ブランチにより置き換えられたもの
これにより、
- 現役作業
- 完了済み研究
- 参考資料 を明確に区別する。
- 本リポジトリのブランチは、論文・ノート・解説文書と 1対1または1対多で対応する
- ドキュメントでは、以下を併記することを推奨する：
- 対応ブランチ名
- 対応コミット ID（短縮可）
例：
branch: thm/cosmic-formula-dim
commit: abc1234- ブランチ名には、以下の接頭辞を用いることを推奨する：
thm/: 定理・補題の証明に関するブランチgen/: 定理の一般化・拡張に関するブランチexp/: 実験的・探索的な試行に関するブランチdev/: 開発中の現在進行形のブランチ
これにより、将来にわたって参照の一貫性を保つ。
- 定理証明の「完成形」だけでなく「構築過程」も研究資産として保存する
- Lean 形式化における試行錯誤を再利用可能にする
- 数学的思考の履歴を、Git の履歴として忠実に残す
本リポジトリにおける Git 履歴は、 証明の副産物ではなく、証明そのものの一部である。
この運用方針は 2026 年 1 月 19 日から適用開始します。 既存のブランチについても、可能な限り本方針に従って管理してください。
- 2026/01/19 10:47 : 初版作成