記事の作り方と検証

Rikai の記事と問題は AI（Claude Code など）が書き、書いた者とは別のエージェントが独立に監査しています。運営者が全体を監修します。そのうえで、定理と証明のつながりは検査スクリプトが機械的に確かめています。このページは、その手順と、検証でわかることとわからないことを書いたものです。人間が証明の 1 行ずつを検算している、という主張はしていません。

1. 執筆

• 章ごとの指示（範囲・主要な定理・閉包の中での役割）をテーマごとに決め、それと執筆規則（定義から積み上げる、証明の各ステップでどの仮定・定理を使ったかを書く、など）に従って 1 章ずつ書きます。
• 定義 → 定理 → 証明 → 例 → 演習（解答つき）の順に書きます。
• 証明の中で使う事実は、(a) その記事の中で補題として証明する、(b) Rikai にある定理を参照する、のどちらかにします。「よく知られている」で済ませません。参照先が Rikai に無ければ、置くべきテーマに章や節を足します。
• 原典の文章や演習は写しません。演習は自作し、参考文献は実在するものだけを挙げます。

2. 独立監査

• 書いた者とは別のエージェントが、記事を 1 本ずつ最後まで読みます。観点は、主張・定義・定理の仮定・証明の各ステップ・計算が正しいか（仮定の欠落、極限交換の無条件使用、循環、場合分けの漏れ、反例）、数式が正しく表示されるか、学部の基礎科目で標準的な内容が欠けていないか、図が要る箇所に図があるか、です。
• 確信できる誤りはその場で直します。直すと構成が大きく変わるものや、判断に迷うものは直さずに報告し、運営側で判断します。
• 結果は「問題なし（pass）」「修正した（fixed）」「未修正の所見が残る（issues）」のどれかで記録します。「未修正の所見が残る」ものは、その旨を来歴に残し、運営側で扱いを判断します。
• 100 本ノックは、監査者が答えを見ずに 1 問ずつ自分で解き、答えと一致するか、正解が 1 通りに決まるか、解説が正しいか、問題が使う定義・定理が Rikai の記事にあり主張が一致するかを確かめます。

3. 来歴（誰が書き、誰が監査したか）

各記事の末尾に、書いた主体（ツールとモデル）、監査の回数、最後に監査した日を表示します。100 本ノックは冊のページに表示します。記録は専用のコマンドで行い、手で書き換えません。

• 初期に一括で公開した記事は、書いた主体を「不明」として扱い、執筆の欄は表示しません。
• 英語版は日本語版とは別に扱っていて、監査の記録が少ないものがあります。来歴の表示が「未監査」の記事は、監査の記録がありません。

4. 命題の閉包の機械検査

Rikai の定理・命題・補題・系は、原則としてすべて Rikai の中で証明されていて、その証明が使う事実も Rikai の中で証明されている（公理や定義までたどれる）ように作っています。これを閉包と呼びます。守るための仕組みは次のとおりです。

• 書き方の決まり: 定理類には証明を付け、証明の中で使う定理は参照の記法（<Ref>）で指します。
• npm run validate: 参照先の定理が実在するか、証明の対象があるか、参照が切れていないかなどを検査します。
• npm run closure: 定理類ごとに、証明があるか、証明の中の参照を推移的にたどって公理まで閉じるかを集計します。
• npm run closure -- --check: 証明のない定理（主張のみ）が、台帳に登録されたものだけかを照合します。台帳に無いものが増えると失敗します。
• CI: 変更を送るたびに、npm run validate と npm run closure -- --check を、図の欠けの検査・型の検査とあわせて自動で実行します。

現況は次のとおりです（ビルド時に数えています。詳しい集計は閉包の状況にあります）。

• 検査の対象は定理・命題・補題・系 9417 件（数学・物理。情報科学とコラムは対象外）。
• うち、証明を持ち、証明が使う定理もたどった先まですべて証明つきのもの（公理まで証明済み）が 9191 件（97.6%）。
• 証明はあるが、たどった先に主張のみの定理がある（または循環している）ものが 38 件。
• 証明を載せていない「主張のみ」の定理が 188 件。台帳の登録は 188 件で、台帳にないものが 1 件でも増えると検査が失敗します。

主張のみの定理と台帳

研究の最前線の結果や、証明が本 1 冊分になる定理は、証明を載せずに主張だけを置くことがあります。その場合は、定理の直後の注意書きに「主張のみ」である理由と出典を書き、台帳（content/closure-baseline.txt）に 1 行登録します。教科書水準の定理は台帳に足さず、証明を書きます。台帳の定理の一覧と理由は閉包の状況で読めます。

5. 定理ごとのページ

定義・定理には個別のページがあり、定理索引から開けます。ページには、主張、その証明が使っている定理（前提の木）、その定理を使っている定理、閉包の状態（✓ 公理まで証明済み／△ 証明あり・閉包未完／※ 主張のみ）、その定理を使うノックの問題が出ます。「この結果は何に依っているか」を、記事をまたいで遡れます。

6. 限界

• 監査も LLM が行っています。 形式証明（証明支援系による検証）ではありません。独立した目で読んでいても、見落としは起こり得ます。
• 閉包の判定は、証明の中に参照の記法があるかに基づく機械的なものです。 証明が参照先を正しく使っているか、証明そのものが正しいかは見ません。参照先が不適切でも、参照が実在していれば判定は通ります。正しさを確かめるのは、監査です。
• 「公理まで証明済み」は、Rikai の中で証明がつながっているという意味です。 主張のみの定理は証明を載せていません。出典を確かめてください。
• 閉包の検査は数学と物理の記事が対象で、情報科学とコラムは対象外です。物理は、基本的な仮定を記事の中で置いたうえで、その先を定理として扱います。
• 以上のため、誤りが残っている可能性があります。

7. 誤りの報告

各記事の末尾の「この記事の誤りを報告する」、またはお問い合わせからお知らせください。どの記事のどの箇所か（記事の URL、定理の番号や行）を添えていただけると確認しやすくなります。確認できた誤りは修正します。

運営の概要はこのサイトについて、全体の構成は学習の地図にあります。