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 にしています。置き場は articles1〜4、ファイル名は問題の番号です（同じ問題の別の本は 52a・52b など）。まずは articles1 の本から見てください（どれも common/word_basis.book を直接 import する1冊完結の本です）。articles2 の本は同じフォルダの word_set（集合と自然数）や op1s（自然数の演算）を、articles3 の本はフォルダの準備 0.book を import します。
同じ定理を、違う前提・違う組み立てで何冊でも書けます。本どうしは独立していて、前提の違いは主張の行で比べられます。

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 の査読で見つかった偽の 〇（高階変数の扱いなど）を直しました（7.book「推論関係とbackend」）。

2 今は弱いところ

使う前に知っておいてほしいことです。
　・ Hyperion（段をつなぐ部分）は発展途上です。正しい証明でも、つなぎ方の規則に無い形だと FAIL します。h の段の 〇 を押すと、段をつないだ記録（どの Thm からどの規則で作ったか）が出ますが、その記録を別の小さな検査器で再生する仕組みはまだありません。
　・ -|（一階に翻訳）と --|（{s,c}ソートのまま）が、どちらも意味を持つときに同値であることは、まだ一般には示していません（5.book）。
　・ 多ソートの Thm を一階の段に使う持ち上げ（multisort→tfl）は、健全性をまだ示していません。使うのは段に h[lift]; と書いたときだけで、これに頼った Thm は、査読の結果に「※ 健全性未証明の規則 multisort→tfl に依存」と、使った定理とともに出ます（articles1/74a の IND𝕄、articles2 の word_set と、その INDC を使う op1s・52b・58a・58b、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 を固定する」「仮定する」のような局所の文脈を書く構文