1 Matheliaでできること

1.1 教科書がそのまま検査の対象になる

Book は、地の文（txt）・記号の紹介（word）・定義や前提（prop）・主張（thm）・確かめ方（prf）を上から並べたものです。表示されるのは教科書の形で、prf は表示されません。
査読は Book を上から読み、その位置までに紹介したものだけで各 Thm を確かめます。紹介していない記号、示していない補題を使えば FAIL です。import した本の結果は、中身が変わっていなければ査読し直さずに使います。

1.2 前提がすべて見える

主張は A ◀ Γ（前提の列 Γ から A が推論できる）の形で、使った前提は Γ に並びます。ただし W. や DB の prop（ax_s など）は名前で並ぶだけで、中身（返り値が s の語の定義が含む「その集合が存在する」という仮定など）は主張の行には出ません。定義も W.（その位置までの定義の列）や名前で Γ に書き、展開は / W. のように書いた通りに行われます。
前提を1つ外すと FAIL になる、ということを実際に確かめられます（1.book の例2・例3）。機械が書かれていない仮定を黙って足すことはしない、が設計の原則です。
例えば articles3/68b.book は、等差数列の和を「可換半環の公理 , 帰納法 , 2 = 1 + 1」という前提から示しています。何を仮定した定理なのかが主張の行に出ます。

1.3 証明の細部は証明器に任せる

prf の各段は「この前提からこの式が出るか」を backend に投げます（p v s の段は中で証明器を使います。h の段はふつう使いませんが、関係をまたいで Thm を確かめ直すときだけ Vampire を呼びます）。人間（AI）が書くのは、補題をどこで切るか・どの定義を開くかという証明の骨格で、一階論理の細かい推論は証明器が探します。
　p; … prover+（Prover9・一階）　v; … vampire+（Vampire・-| でも --| でも）　s; … satallax+（Satallax・高階）　h; … hyperion（段をつなぐメタ推論。式の証明探索はしない）
例：Cantor の定理（articles1/63.book）は、X ≤# ℘ X（単元集合への単射の段を証明器に投げる）と X ≠# ℘ X（対角クラスが |X の部分であること〈LAs〉と、写像が全射でないこと〈LeA〉の段を投げる）を別々の Thm にし、どちらも定数 |X（2つ目は写像 |f も）で示したものを h[fix]; の段で変数の主張に戻します（1つ目は最後の段 goal -| W. , ax_s h[fix];、2つ目は途中の段 Lgen）。単射・対角クラスに付けた集合の名前 |g・|A は、この段で ∃除去により消えます（6.book）。主定理 `X <# ℘ X` ◀ W. , ax_s の prf は、この2つを引く2行です。
段のつなぎ方（合成・slash の除去・∀導入など）は決まった規則で、3.book「h; がすること」に一覧があります。

1.4 実例：Freek の100定理

Freek の100定理（形式化の進み具合の物差しによく使われる一覧）のうち、次を Book にしました。どれも共通の準備 0.book（論理〜分出公理・articles1〜3 に同じものを置いています）を土台にしています（2026-10-04 に査読 ALL OK）。#52・#58 は集合で自然数を作る準備 articles2/0-sn.book（Thm 30件）を、#1・#3・#10・#11・#23・#31・#44・#60・#66・#68・#69・#73・#80・#85 は自然数を公理で与える準備 articles3/0-pa.book（Thm 65件・強い帰納法 SIND𝕄・冪 ↑・偶奇 𝕄偶奇〈𝕄 = 2⋅𝕄 ∪ (2⋅𝕄+1)・証明用の隠し Lpar／Lne〉・順序と整除の補題〈⋅K・L　#23 ピタゴラス数（articles3/23.book・Thm 1件・互いに素で \(b\) が偶数なら \(a + n^2 = m^2\)・\(b = 2mn\)・\(c = m^2 + n^2\)・補題「共通の素因数を持たない2数の積が平方数なら平方数」は 23-1・Thm 3件〈80-1・11 を import〉・2026-10-06）
　#25 Cantor-Schröder-Bernstein の定理（articles1/25.book・Thm 7件）
　#63 Cantor の定理（articles1/63.book・Thm 9件）
　#52 部分集合の個数（集合 n の部分集合 articles2/52a.book・Thm 4件、n と対等な任意の集合に広げた 52b・Thm 2件）
　#74 数学的帰納法（articles1/74.book・Thm 1件）
　#68 等差数列の和（自然数を公理で与える articles3/68a.book・Thm 1件、可換半環の公理から示す 68b・Thm 1件）
　#11 素数の無限性（articles3/11.book・Thm 4件・自然数を公理で与えたユークリッドの証明・2026-10-05）
　#11 素数の無限性・別証明（articles3/11b.book・Thm 6件・フェルマー数 \(F_n = 2^{2^n}+1\) の相異なるものは共通の素因数を持たない〈\(m \lt n\) なら \(F_n = F_m Q + 2\)〉ので、\(n\) ごとに新しい素数がある・import 11 80-1・2026-10-07）
　#1 √2 の無理性（articles3/1.book・Thm 4件・\(m^2 = 2n^2\) なら \(n = 0\) を無限降下で・系 √2∄・2026-10-05）
　#58 組合せの数（articles2/58.book・Thm 3件・k 元部分集合は \(n \mathrm{C} k\) 個・2026-10-05）
　#69 互除法（articles3/69.book・Thm 2件・引き算型の漸化式で与えた \(a \gcd b\) が公約数で、どの公約数でも割り切れる・2026-10-06、そういう最大公約数が存在することを \(a + b\) の強い帰納法で示した 69b・Thm 1件・2026-10-08）
　#60 Bézout の定理（articles3/60.book・Thm 1件・69 を import・引き算なしで \(as = bt + a \gcd b\) か \(bt = as + a \gcd b\)・2026-10-06、整数で \(as + bt = a \gcd b\) と述べた articles4/60b.book・Thm 1件・整数の準備 articles4/0-z.book〈standard_math/1-4 の上・強い帰納法 SINDC など Thm 7件〉を import）
　#80 素因数分解の存在と一意性（articles3/80.book・Thm 9件・昇順の素数の列とその積で・ユークリッドの補題は articles3/80-1.book を import・2026-10-06）
　#3 有理数の可算性（articles3/3.book・Thm 3件・\(2^a(2b+1)\) の表し方の一意性から 𝕄 から ℚ への全射、Calkin–Wilf 列（fusc）で示した 3b・Thm 4件・2026-10-07）
　#66 等比数列の和（articles3/66.book・Thm 1件・和を漸化式で与え \(r s_n + a = s_n + a r^n\)・2026-10-07）
　#85 3の倍数の判定法（articles3/85.book・Thm 5件・桁の列 \(d\) で \(N = \sum d(i)\,10^i\)・\(S = \sum d(i)\) を漸化式で与え \(3 \mid N \Leftrightarrow 3 \mid S\)・補題 \(10^i = 3c+1\)・2026-10-07）
　#44 二項定理（articles3/44.book・Thm 3件・和を \(s(k+j)(k+1) = s(k+j)(k) + \binom{k+j}{k} a^k b^j\) で与え \((a+b)^n = s(n)(n+1)\)・要は \(s(n+1)(m+1) = b\,s(n)(m+1) + a\,s(n)(m)\)・2026-10-07）
　#73 Erdős–Szekeres の定理（articles3/73.book・Thm 16件・相異なる \(n^2+1\) 個の数の列は長さ \(n+1\) の増加か減少の部分列を持つ・各位置で終わる最長の増加・減少部分列の長さの組を鳩の巣原理 PH に当てる・2026-10-07）
　#10 Fermat の小定理（articles3/10.book・Thm 4件・\(p\) が素数なら \(a^p = a + pq\)〈自然数に引き算が無いので合同式を使わない形〉・\((k+1)\binom{n+1}{k+1} = (n+1)\binom{n}{k}\) から \(p \mid \binom{p}{k}\)・44 の二項定理を \(b=1\) で引き \(a\) の帰納法・2026-10-07）
　#31 Ramsey の定理（articles3/31.book・Thm 8件・どの \(P, Q\) にも、頂点が \(N\) 個以上なら2色の塗り分けに大きさ \(P\) の赤か大きさ \(Q\) の青の完全部分がある \(N\) がある・\(P\) と \(Q\) の二重の帰納法・2026-10-08）
同じ定理を、違う前提・違う組み立てで何冊でも書けます。本どうしは独立していて、前提の違いは主張の行で比べられます。

1.5 AI のための道具

画面を持たない AI でも、すべて CLI で作業できます（場所は /var/www/test2.atp-research.com、コマンドは wp-content/themes/lightning/ からのパス）。
　mathelia/review_cli.php <本> … Web の「査読」と同じ査読。終了コード 0＝ALL OK／1＝FAIL あり／2＝引数の誤り／3＝判定できない。--inputs で、落ちた段について prover+ などが受け取ったもの（翻訳した後の式）と、証明器に投げた入力を出す
　mathelia/slash_cli.php <本> '`式` // W.' … 式の読まれ方と slash の展開を、証明器に投げずに見る
　.claude/prf_trial.php <本> <Thm の行> <候補> … … 1つの Thm に prf の候補をいくつも当て、通ったか・PHP と証明器の秒・長さを JSON で返す（本は書き換えない）。--quick で結論のつなぎを省いた速い試し
　mathelia/ai_reading.php <本> … … 本の表示（読者が見る文章）とソースを並べた、読むための資料を作る
FAIL の理由は日本語の文で返り、どの語・どの行・どの段かを指します（例「本が紹介していない word を Form の中で使っています: +」）。

1.6 〇 を説明できること

一つの OK（〇）について、書かれた Thm・各段の変換・すべての前提と出所・証明器に渡した入力・結果まで追えることを、いちばん大事にしています。
査読器そのものも疑われる対象です。偽の 〇（通ってはいけないものが通る）の実例は反例集に貯め、直した後も毎回落ちることを確かめます。2026-10-04 には、外部の AI の査読で見つかった偽の 〇（高階変数の扱いなど）を直しました（HOL.book「推論関係とbackend」）。

2 今は弱いところ

使う前に知っておいてほしいことです。
　・ Hyperion（段をつなぐ部分）は発展途上です。正しい証明でも、つなぎ方の規則に無い形だと FAIL します。h の段の 〇 を押すと、段をつないだ記録（どの Thm からどの規則で作ったか）が出ますが、その記録を別の小さな検査器で再生する仕組みはまだありません。
　・ -|（一階に翻訳）と --|（{s,c}ソートのまま）が、どちらも意味を持つときに同値であることは、まだ一般には示していません（5.book）。
　・ 多ソートの Thm を一階の段に使う持ち上げ（multisort→tfl）は、健全性をまだ示していません。使うのは段に h[lift]; と書いたときだけで、これに頼った Thm は、査読の結果に「※ 健全性未証明の規則 multisort→tfl に依存」と、使った定理とともに出ます（articles2 の 0-sn・52a・52b・58＝0-sn の INDC を使う本、standard_math の 1-3・1-4・2-def＝1-3 の INDC を使う本）。
　・ 証明器の「証明できた」は、その証明を Mathelia の外の検査器で確かめ直してはいません。
　・ word の文法や DB に登録された定義（prop ax_s など）の本文は .book ファイルの外にあります。.book だけを別の機械へ持っていっても、意味は閉じません。
　・ サーバが小さく（メモリ 1GB）、重い Book の査読は遅いです。

3 これから入るもの

3.1 決まっていること・進めていること

　・ サーバを移します（近いうち）。査読が速くなる見込みです。
　・ Freek の100定理の本（articles1〜4）を、公開できる水準まで磨きます。
　・ Hyperion のオプション（h[〇];）を設計しています。書いた段でだけ効く強い規則（例：有界な内包を分出公理で集合と認める h[sep]）で、どの段が強い推論に頼ったかが綴りに出ます。この一部（集合に名前を付ける仮定を、分出公理などの根拠で消す）は h[fix]; の ∃除去として入りました（6.book）。強い規則でも、何をしたかを基本の規則の列として記録し、小さな中核で確かめ直せる形にする方針です。
　・ 長期の目標は、Fermat の最終定理（Freek #33）を記述することです。基礎から順に進めます。

3.2 検討中の候補

外部の AI の感想から出た候補です。まだ決まっていません。「こういう機能が欲しい」という意見を歓迎します。
　・ DB の定義・記号の文法まで含めた、単独で読める「展開済みの本」の書き出し
　・ 査読結果の機械可読な出力（行・段・規則・依存関係・翻訳後の式を JSON で）
　・ FAIL の種類（書き方の誤り・反例・時間切れ・つなげない）を結果の中で分けて出す
　・ 定理ごとの前提一覧（W. の中身、存在を仮定している定義）の表示
　・ 「任意の x を固定する」「仮定する」のような局所の文脈を書く構文