【訂正】Astra数学記事：成果・換算費用・検証を分ける

訂正：研究の成果と費用を広く言い切っていた

8月7日の旧稿は、Astraが「数学の未解決問題10問を解決した」と題名に掲げていました。一方、本文では「解決または大きく前進」と説明しています。すべての問題を解決したことと、進展を含む成果があることは同じではありません。題名とまとめで達成範囲を広げた説明を取り下げます。

9月5日の今回の精査では、旧稿が根拠にした8月1日の元告知と、個別の論文・証明ファイルを開いて再確認できていません。以下の処置は「研究が存在しない」「数学的に誤りだ」と判定したという意味ではなく、今回の裏付けがない断定を残さないための訂正です。

旧稿の説明	今回の扱い
未解決問題10件を解決	各問題の達成範囲を未再確認。「前進」まで一律に解決としない
個別の定理・問題番号・専門用語の訳	元論文と対応を再確認できていないため、確定した成果一覧として再掲しない
推論の総費用が約2,000ドル	旧稿内でも別モデル料金による換算と記載。支払実費や総事業費に読み替えない
人間の論文化、モデルによるLean検証、過去研究との関係	元の手順・対象・分担を未再確認。今回確認した実績とはしない
非公開モデルなので一般には使えないという当時の案内	8月時点の説明を現在へ延長しない。現行の案内と研究用モデルを分ける

現在はGPT-6 Astraのモデル資料にAPIのモデル名や料金条件が掲載されています。ただし、その資料から過去の研究用内部版と同一条件だったとは判断できません。読者のアカウントでの利用可否や、元研究の再現性も、ページの存在だけでは確認できません。

表紙はAI生成の概念イラストです。元研究の図、証明結果、研究用モデルの出力を再現したものではありません。

料金換算は、支払実費や業務単価ではない

旧稿は、使ったトークンをSol API料金へ換算したという説明を置きながら、後段では「総推論コスト」と呼び、10で割った金額を別の高難度業務へ使う目安にしていました。この推論は撤回します。元のトークン数・単価・集計対象を今回照合できておらず、モデルを動かした実費を測定したものでもありません。

換算額を読む際は、少なくとも「何の量を」「いつのどの料金で」「どの範囲まで」計算したかを残す必要があります。成功した出力だけなのか、失敗した試行や検証の処理まで含むのかによって意味が変わります。人の確認・修正にかかった費用を含むかどうかも別項目です。未記載ならゼロとして足し合わせません。

また、研究課題の件数で割った平均は、別の仕事1件の見積額にはなりません。契約文書や財務・統計上の判断を低費用で代替できることも、本稿では検証していません。旧稿の具体的な業務への推奨は取り下げ、実際に使う場合の対象・成功条件・確認者を先に決めるという案内に変更します。

検証の違い：40例の成功でも、全体の証明にはならない

Leanの公式検証ガイドは、「定理の証明が有効か」と「その定理文が何を意味するか」を区別しています。検証されるのは、定義・定理・公理に基づく形式化された主張です。意図した元の問題とその主張が一致するか、依存する前提に問題がないかは別に確認します。同ガイドは、依存先の未完了部分が sorryAx として検出されることなども説明しています。

これは、リンクの有無や必須項目を調べる当ブログの記事検査とは保証する対象が異なります。記事が機械検査を通っても、数学の証明や出典の正確性が保証されるわけではありません。旧稿で両者を近いものとして説明した箇所は訂正します。今回、Leanの証明検査を実行したわけでもありません。

違いを手元で確かめるため、研究とは別の小さな算術例を実行しました。n*n+n+41 が素数になるかを、最初は整数n=0から39まで、次にn=40で調べます。Python 3.14.2／Windowsで実行し、外部API・追加ライブラリ・費用は使っていません。

次のコードを math_check_boundary.py として保存し、そのフォルダで python math_check_boundary.py を実行できます。大きな数の高速判定用ではなく、この小さな入力のための試し割りです。

from math import isqrt

def is_prime(value):
    return value >= 2 and all(
        value % divisor != 0
        for divisor in range(2, isqrt(value) + 1)
    )

def polynomial(n):
    return n * n + n + 41

passed = sum(
    is_prime(polynomial(n)) for n in range(40)
)
print("n=0..39:", passed, "/ 40 prime")
print("n=40:", polynomial(40), "= 41 * 41")
print("n=40 prime:", is_prime(polynomial(40)))

実行結果は次のとおりです。

n=0..39: 40 / 40 prime
n=40: 1681 = 41 * 41
n=40 prime: False

最初の40個はすべて素数でしたが、次は41×41で割り切れます。「n=0から39の範囲では条件を満たす」という確認結果は保たれます。一方、「すべての非負整数nで素数になる」という主張にはn=40が反例です。有限範囲を全部調べた結果を、その外側まで保証する結果へ広げてはいけません。

これはAstraの誤答を検出した例でも、Leanの代わりとなる証明でもありません。こちらで用意した式と入力を計算しただけです。例の成功件数を、元研究の信頼性を測る数値に使わないでください。

実務への影響：研究ニュースを使う前の確認票

研究成果を業務へ結び付ける前に、次の5項目を分けて残します。本稿の訂正で得た、読者向けの確認票です。

確認する項目	残す証拠・条件
何が達成されたか	対象問題、解決・反証・部分的進展の区別、元論文
どのモデルか	研究用内部版か現行製品か、版・設定・人間の介入
費用は何を表すか	実費か料金換算か、単価の時点、試行と確認工程の範囲
何を検証したか	形式化した主張、前提、検証器・依存物・実行結果
自分の仕事にも当てはまるか	入力、成功条件、確認者、未検証の範囲

元論文を読めていなければ、概要だけで問題名や数学用語を補いません。証明ファイルの存在を確認しただけなら、「自分でも検証した」と書きません。費用の対象範囲が欠けていれば、その額を社内の見積単価へ転記するのを保留します。

当ブログでも、機械検査が通ったことと、出典を再確認したことを別々に記録します。実行結果を判断材料へまとめる考え方は、意思決定フローを回した記録にもつながります。いずれも特定条件の記録であり、あらゆる判断をAIへ任せられるという保証ではありません。

今回完了したのは原稿の不一致の点検、断定の撤回、公式ガイドの照合、小さな数値例の実行です。元研究の証明・数学用語の訳・成果件数・費用を全面的に再検証したわけではありません。既存URLの訂正として残し、新たな研究成果や実機レビューとして数えません。