仕事の総論
・推論のシステム、ライブラリ、を作る。
使いやすいソフト、人間にとっても美しい教科書、になるよう心がける。
・新しい数学世界を作る。
新しい定理を作るのではなく、数学の枠組みを変える。
現在、抽象数学の初歩を追認できるレベル。数学者の相棒と言えるくらいにはならないと。証明のチェックって大変らしいので、その補助ができるように。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を作る？土屋さんのシステムで？
開発に当たって
・大きなビジョンを共有しつつ、短期的な目標を立てて実行していく。
「何を作るのか」言語化する。
動くものを早く作る（アジャイルな姿勢）。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