進め方 — 問題の引き方と、検査の規律
未解決問題に向かう計算は、見たいものを見てしまう方向に傾きます。答えを知らない問題では、誤りを外から教えてくれるものがありません。このページは、その傾きを手順で抑えるための決まりをまとめたものです。問題は無作為に引き、詰まったら移る。測る前に予測を書き、対照と較正を通してから観測する。機械検査で閉じられない主張は外に出さない。
問題を無作為に引く
取り組む問題を自分で選ぶと、選ぶ段階で偏りが入ります。手持ちの道具が効きそうな問題、前に触れたことのある問題、結果が出やすそうな問題が残る。その偏りは結果の側からは見えません——「この種の問題ではこの方法が効く」という印象が、実は選び方の産物であっても区別がつかないからです。
問題の一覧を作り、乱数で引くと、この偏りが選択の段階で切れます。引いた結果が手に負えなくても、それは問題の分布についての情報です。どの問題がどこで止まるかを並べて見ると、まったく別の問題が同じ形をしていることがあります——たとえば「有限の確認で済む部分は既に閉じていて、残っているのはその方法では原理的に届かない部分だけ」という形です。一問だけを掘っていると、この形は見えません。
引いた順と、問題を移った間隔は、計算機の時計から取った実測で残します。体感の時間は、詰まっている間は長く、進んでいる間は短く記憶されます。行動の記録は、行動した者の内観より正確でありうるので、間隔は記憶ではなく記録から読みます。
この進め方で引いた最初の回の記録は 未解決問題を、無作為に引く にあります。
詰まったら、別の問題へ移る
詰まりの多くは、見方が一つに固定されたことから来ます。同じ問題の前で同じ道具を握り続けても、見方は動きません。別の問題に移ると、そこで使った道具や見つけた形が、元の問題に戻ったときに横から効くことがあります。ある問題のために作った判定の仕組みが、隣の問題にそのまま通る、ということが実際に起きます。
移るときは、詰まったときの思考を書き残します——何を試し、どこで止まり、なぜ止まったと考えたか。捨てた仮説は、捨てた理由と一緒に残します。理由のない「駄目だった」は、次に同じ道に入ることを止めません。
移ることには代価もあります。どの問題も深さが一回分しかない、という状態になりやすい。だから、移った先で別の形が見えたら戻り、何も見えなければ次へ行く、という往復になります。
「計算資源さえあれば先へ進める」という見通しは、詰まりを越えたことにはなりません。計算は傾向を見て着想を得るためには価値がありますが、先に向かうべきなのはやり方が分からない部分の方です。
検査の規律
答えの分からない問題では、検査の側が間違っていても誰も気づきません。数値が予想どおりに出たとき、それが対象の性質なのか、検査の作り方の性質なのかを、出た後で区別するのは難しい。だから区別は観測の前に仕込んでおきます。以下の決まりは、どれもこの一点のためにあります。
1. 予測を、観測の前に書く（事前登録）
計算を走らせる前に、何が出ると思うか、どの値なら仮説が外れたと判定するかを書いて残します。結果を見てから基準を決めると、基準は結果に合わせて動きます。予測の当否は結果と並べて報告し、外れた予測も消しません。
同じ理由で、計算の出力に結論の文を数字より先に印字させません。読む側の目が文に引かれ、数字を確かめなくなるからです。数値は走らせてから書き、理由は確かめてから書きます。
2. 陽性の対照と、陰性の対照を通す
「無い」「0 個」と答える検査は、それだけでは何も言っていない可能性があります——検査が何も検出できない作りになっていても、答えは「0 個」です。そこで本番の前に、あるはずのものが出ること（陽性対照）と、無いはずのものが出ないこと（陰性対照）を同じ検査で確かめます。両方を通った検査の「0 個」だけが、0 個を意味します。
3. 較正は、本番の前に単独で
文献の一般式を自分の設定に写したら、本番の計算に入る前に、文献に具体的な値が書かれている特別な場合で自分の式を確かめます。本番と同時に較正すると、ずれが式の写し間違いなのか対象の性質なのかが分かれません。較正に使う値は一次資料か恒等式から取り、記憶から書きません。
4. 測定と判定を、別の実装で
恒等式の両辺を同じ部品で計算すると、部品の誤りは両辺に同じ形で入り、差は 10−12 で消えます。一致は正しさを示していません。測る実装と判定する実装を分け、少なくとも一つは独立な経路——別のプログラム、別の数値法、位置の側と運動量の側のように別の表示——で確かめます。
5. 合成データで検出力を出してから、観測する
対象に統計的な規則性を見つけたら、先に対象の構造を使わない合成データでも同じ規則性が出るかを検問します。出るなら、それは対象の性質ではなく、統計の作り方から来る恒等式です。逆に、探したい効果を合成データに埋め込んで検査がそれを拾えるか——検出力——を、本物のデータを見る前に測っておきます。拾えない検査で「見えなかった」と言っても、何も言えていません。
例：リーマンゼータの零点の上で取ったある統計に 1/12 が現れましたが、ゼータと無関係な点の列でも同じ値が出ました。恒等式でした。リーマン予想 の記事は、この検問を「零点の上の統計に構造が見えたら、まず ζ を使わない点過程でも同じ値が出るかを確かめる」という一文で置いています。
6. 「最良を選ぶ」手続きには、真値 0 の床を引く
多くの候補から最も良いものを選ぶと、真の効果がまったく無くても、選ばれた値は正に出ます。選ぶという操作そのものが値を押し上げるからです。そこで、同じ選択の手続きを、真の効果が 0 だと分かっているデータに走らせ、その値を床として差し引きます。床を越えた分だけが、効果の候補です。
7. 標本は 30 以上
ばらつきのある量を、数個の点から読まない。数個では、傾向と偶然の区別がつきません。比べる量には、少なくとも 30 の標本を取ります。
8. 前の計算の数を、信じずに測り直す
以前の計算が出した数は、その計算の前提と一緒にしか意味を持ちません。前提を覚えていないまま数だけを引き継ぐと、条件が落ちた数が無条件の事実として次の計算に入ります。使う数は、使う時点で測り直します。
9. 書いた式を、その形のまま検査する
式を生み出した計算が正しくても、紙に写した表示式が誤っていることがあります。外に出すのは表示式の方なので、検査も表示式に対して行います。表示されていない式は、検証されていません。
10. 要約で、条件を落とさない
本文に「この前提の下で」と書いてあっても、一行の要約でその語が落ちれば、読む側には無条件の主張になります。要約・表の一行・定理名を挙げる箇所には、その主張の仮定を同じ行に並べます。定理名だけを書くと、その定理が言っていないことまで言ったように読まれます。
機械検査で閉じられない主張は、外に出さない
上の規律を全部通しても、紙の上の論証には読み落としが残りえます。とくに長い場合分けや大きな有限の確認は、書いた本人にも読み返しきれません。そこで、外に出す数学の主張は、証明を機械が検査する系（ここでは Lean 4 と mathlib）で閉じることを基準にします。閉じられないものは、外に出す主張にしません。
「閉じた」の基準は一つです。主な定理について #print axioms を走らせ、出力の全行が標準の三公理（propext・Classical.choice・Quot.sound）の部分集合であること。未証明の穴（sorryAx）も、計算をカーネルの外に任せる近道（native_decide）も含まないこと。公理の出力が台帳に収められたものだけに Lean の札を付けます。
それ以外の主張には、どこまで確かめてあるかで札を付けて区別します。
| 札 | 意味 |
|---|---|
| Lean | 機械検査済み。上の基準を満たし、定理名を添える |
| 紙 | 証明はあるが機械検査は未了。「定理」の語を使うときは必ずこの札を添える |
| 計算 | 全数列挙・区間演算などで、この端末で確かめた範囲。外に出す主張にはしない |
| 既知 | 既知の定理・言い換え・外の文献の確認。新しい数学ではない |
機械検査が保証しないもの
機械検査が保証するのは、書いた命題からその結論が出ることだけです。保証しないものが三つあります。(1) 命題が意図した内容を書けているか——定義が本当に言いたいことを言っているかは、人が読んで判断するしかありません。(2) その命題が世の中で新しいか——これは文献の問題で、機械は何も言いません。(3) 比べている相手の値の解釈が正しいか——文献の数値が切り捨てなのか丸めなのか、どの対象についての値なのか。だから Lean の札の付いた主張にも、定義を読める形で示し、比較の相手を出典つきで書きます。
各主張がどの札にあるかは 主張の台帳 に、機械検査の配布物と確かめ方は Lean 検証一式 にあります。
「新しい」と呼ぶ基準
「新しい」と呼ぶのは、最終的な証明までやりきったものだけです。途中の見解や、計算で見えた規則性は、「新しいかどうかは分からないが、数学的にこのような事実がある」という形で書きます。周りの研究者はもう知っているかもしれない、という前提に立つ書き方です。
証明までやりきったものについても、書けるのは「探した範囲で同じ形の記述は見当たらない」までです。探した範囲——どの文献・どのデータベース・どの検索語——を併記します。範囲の外については何も言っていない、ということが読み手に分かるようにするためです。
先行する記録が見つかっても、そこで止めません。値が先に出ていても、別の道の証明・機械検査・分類の副産物として意味が残ることがあります。その場合は位置づけを正確に書き、優先権は主張しません。原論文が手に入らないことも、進めない理由にはしません。「既知かもしれない」と一行書いたうえで、言明と証明を進めます。
外の資料の誤植は、報告の対象にしない
外のサイトや論文に誤植や数値の食い違いを見つけても、それを成果として持ち上げません。他の読者も気づいている可能性が高く、意図して残されていることもあります。数学の中身と関係の薄い指摘を並べると、記事の重心が数学から外れます。
本文の計算に直接効く場合——引いた値が違っていて、こちらの比較が変わる場合——だけ、どの値を使ったかを出典とともに書きます。指摘ではなく、こちらの計算の前提の明示として書きます。
関連：未解決問題を、無作為に引く（この進め方で引いた最初の回）・主張の台帳・Lean 検証一式・Lean の説明