仕事の総論
・推論のシステム、ライブラリ、を作る。
使いやすいソフト、人間にとっても美しい教科書、になるよう心がける。
・新しい数学世界を作る。
新しい定理を作るのではなく、数学の枠組みを変える。
現在、抽象数学の初歩を追認できるレベル。数学者の相棒と言えるくらいにはならないと。証明のチェックって大変らしいので、その補助ができるように。ABC予想の懸賞金を取りに行く？定義が多くこまごましたものは、機械がやるべき。
ライブラリ
とりあえず、Fermatの最終定理までをなるべく寄り道しないで与える。
大事な分野・重要事項のみを選び、スマートな道を通していく。
・2026年5月…濃度の計算
・2026年6月…構造付き集合
・2026年7月…\(\mathbb{Z}\)
・2027年…学部数学で必要なもの
・2028年…FLT
Kevin Buzzard教授のLeanプロジェクト参考になるかも。
ある程度基盤ができたら、数学の諸分野について、色々な人に書いてもらう形に？
システム
・一階言語の拡張でFormを作る言語。
それとは別に、\(\blacktriangleleft\)の注釈にあるようなTrainを作る言語。
・どちらの言語も拡張、整備をすべし
・Trainを定理チェックに入れるとproverが証明してくれる。
phpがprover語まで翻訳した上でproverに渡している。
・圏(category)を扱えるように。超準解析も。
・proverにmax_proofオプションのバグあり？
・Vampire, E, Z3などの方が良い？
多ソートに対応している。入力形式が国際標準。拡張性も高い。
・prover9で多ソート論理をやらせると推論のたびに「xは集合か？」といったチェックが走り検索空間が爆発する。
・型理論を使うLeanなどにはとりあえず触れない。
・数学をやるソフト？
php自体でMathPHPというライブラリを利用する or phpからSymPyを叩く or WolframAlpha,MathematicaなどをAPI経由で利用する
証明補助
・Trainは長くなることも多く、作るのは一苦労。
・コンピュータ将棋のように探索をできるようになって欲しい。
php自体で、定理の候補をたくさん生成する？それをどんどんProverに問い合わせる。
「真」に近いかどうか、評価関数作れる？AIなら？
・Trainを作成する能力に特化したがAIが欲しい
数学書や論文からtex混じりの自然言語を読み取ってtxtを作れる？
・会話しながらTrainを作る？土屋さんのシステムで？
AI利用
開発補助
⓪chatgpt等を導入
①システムを勉強させる
②システムについて会話（構文チェックなど）
③システムの改訂（コード作成など）
証明補助
証明の一つのやり方…何らかの言語で書かれた証明(の方針)をProver語に翻訳してProverに渡す。
その一部を実装済…\(\blacktriangleleft\)の注釈にあるtxtを定理チェックに入れるとproverが証明してくれる。
txtは長くなることも多く、作るのは一苦労。
・（実装済システム内でもそれ以外でも）コンピュータ将棋のように探索をできるようになって欲しい。
・数学書や論文からtex混じりの自然言語を読み取ってtxtを作れる？
開発に当たって
・大きなビジョンを共有しつつ、短期的な目標を立てて実行していく。
「何を作るのか」言語化する。
動くものを早く作る（アジャイルな姿勢）。1〜2週間単位の短期目標を立て、小さな「できた！」という成功体験を積み重ねる。
→モチベーション維持、困難に直面したときの粘り強さ
・「泥臭い改善」と「枠を超える発想」の共存
地道な積み重ね、地味な作業で堅牢な土台を作る。
既存のやり方に固執せず、「全く別の技術で解決できないか？」と問い直す。煮詰まったときこそ、遊び心のある大胆な発想がブレイクスルーを生む。
・多様なツールを柔軟に活用する
難しくも大事で面白いこと。
難関大の入試数学は諸単元の融合問題が出されることが多い。抽象数学の有名な定理では一見関係のない諸分野の結果が使われることも珍しくない。機械による証明でも、許される操作を適切に組み合わせるのがミソ。
現代では本当に様々な道具がある。システム開発でも、良いものは何でも使う。
SQLメモ
UPDATE `wp_waffledb_Prop` SET txt=REPLACE(txt,"P%","%_");
UPDATE `wp_waffledb_word0` SET Form=REPLACE(Form,"<=","|=");
メモ
TPP 2025: 21st Theorem Proving and Provers Meeting, Dec 3 Wed - 4 Thu, Tohoku University
TPP 2024 at Kyushu University
Formalizing 100 Theorems
機械数学でのAI利用 chatgptに聞いてみた
人間がやっていた細かい証明作業や探索を、システム側に肩代わりさせる。
今までの自動化
レベル１．タクティックによる自動化
Leanにはsimp(簡約)、ring(代数計算)、linarith(線形不等式)のようなタクティックがある…人間がやると面倒な計算や整理を自動化
ただし「どのタクティックを使うかは」人間が決める。
レベル２．証明探索（クラシックATP）
システムが使えそうな定理を列挙、適用パターンを試す、ゴールに到達するまで探索…自動証明器
探索空間が爆発する、どの定理を使うかの選択が難しい。
最近：AIとの統合
①次の一手の予測 AIが「このゴールならこの補題を使いそう」「この形ならこの変形」を確率的に提案…人間の直感の代替
②証明の骨格の生成 まず補題Aを使う、次に帰納法、最後に既存定理Bで閉じる、などという戦略レベルを出す
③自然言語→形式証明 数学の文章→Leanコードに変換…人間の作業を直接削減
④失敗から自己修正 証明を書く→Leanがエラーを出す→AIが原因を推定→修正して再試行 をループで回す。
なぜLean系と相性が良いか
型理論ベース（Leanなど）は、状態が完全に形式化されている、ゴールが明確、エラーが厳密…AIにとって学習しやすい
Mizarなどの自然言語寄りは、曖昧さが残る、内部状態が扱いにくい…AIが扱いにくい
DeepSeek-Proverはまさに、証明探索（ATP）、戦略生成、修正ループを全部AIでやろうとする試み。
これからの抽象数学…証明の「労働部分」が機械化
人間：発想・構造設計
AI：証明探索・実装
システム：検証
論理的探索（従来ATP）と統計的予測（AI）をどう組み合わせるか、今まさに主戦場
Mizarについて
Mizarというシステムは、ChatGPTのように「AIが証明を生成してくれるツール」というよりは、「人間が書いた証明に論理的な穴がないかを、コンピューターが厳密に査読するツール」だと考えるのが正確です。
具体的に、人間が何を行い、Mizarが何を返すのかを整理しました。
1. 人間がすること
人間はエディタ（VS Codeの拡張機能など）を使って、以下のすべてを記述します。
- Environ（環境部）: どの定義や定理をライブラリから持ってくるかの指定。
- Theorem（定理の主張）: 何を証明したいか。
- Proof（証明の本文）:
let,assumeなどのキーワードを使い、論理のステップを一行ずつ記述します。
2. Mizar（システム）がすること
人間が書いたファイルをMizarのチェッカー（mizfなど）にかけると、システムは上から順に論理を検証し、エラー（Error）だけを出力します。
- 論理の飛躍がある場合:
*4（推論が成立しない）などのエラー番号を表示。 - 定義が見つからない場合:
*7（未知の識別子）などを表示。 - 正解の場合: 何も出力されません（No errors detected）。
**「便りがないのは良い便り」**というのがMizarの世界です。すべてが正しく記述できれば、エラーが消えて「証明完了」となります。
3. なぜ「AIによる数学」と言われるのか？
「人間が全部書くなら、AIではないのでは？」と思われるかもしれません。ここが研究の面白いところです。
過去のスタイル
以前は、人間が数ヶ月かけてMML（ライブラリ）の定理を調べ上げ、一歩ずつ手書きで証明していました。
現代のAI研究（Mizar + AI）
最近の研究では、この「人間が書く部分」をAIに代行させる試みが盛んです。
- Premise Selection（前提選択）: 膨大なMMLの中から、証明に必要な定理をAIが自動で探し出す。
- ATP (Automated Theorem Proving): AIが
proofとendの間を自動生成する。 - Mizar-to-AI: Mizarの「人間に読みやすい」という特徴を活かし、大規模言語モデル（LLM）にMizar言語を学習させ、自然言語の数学論文をMizarコードに翻訳させる（Autoformalization）。
実際の作業フロー（イメージ）
- 人間: 「$A = B$ の証明を書いたぞ。チェックしてくれ」とファイルを渡す。
- Mizar: 「3行目から4行目への推論が飛んでいます。エラー
*4です」 - 人間: 「（中間のステップを1行書き足して）これならどうだ？」
- Mizar: 「エラーなし。証明完了です！」
このように、Mizarは「絶対に妥協しない厳しい数学の先生」のような役割を果たします。