中国の浙江大学・清華大学などの研究チームが、超伝導量子プロセッサーで幾何の証明手続きを実行した。対象は正方形の対角線が直交するという定理と、1978年の国際数学オリンピック（IMO）の問題である。2026年9月13日に公開されたプレプリントは、従来のコンピューターで研究されてきた自動定理証明を、量子回路で動かす実験を報告している。新しい数学的真理や計算速度の記録ではなく、証明のどの操作を量子ハードウェアが担えるのかを問う成果だ。

AD

既知の幾何問題を量子回路で証明する

Ning Wang氏、Zheng-Zhi Sun氏らが使ったのは、121量子ビットを備えた超伝導プロセッサーである。研究はarXiv:2609.14533として公開されており、現時点では査読済み論文としての評価が確定したものではない。実験の対象も、性質の異なる二つの幾何問題に絞られている。

1978年から2026年までは48年ある。ただし、今回扱ったIMOの問題が48年間未解決だったわけではない。研究者が試したのは、既知の結論に至る証明操作を量子回路へ組み込み、実機でその推論を進められるかどうかだった。

自動定理証明では、図を見て「おそらく正しい」と判断する代わりに、前提と許された規則から結論を導く。幾何なら、辺が等しいことや直線が垂直であることを、数式や記号の関係として扱う。途中の式が複雑になり、試すべき推論の候補が増えると、計算に必要な時間や記憶容量が膨らむ。

そこで研究チームは、異なる二つの経路を実装した。正方形には、図形を多項式へ置き換える「呉の方法」を使った。IMO問題では、角の関係を順につなぐ証明探索を試した。前者は決められた順に式を簡約し、後者は用意された規則から次に適用するものを選ぶ。

正方形の証明を多項式の計算に変える

正方形の実験では、頂点の座標を変数で表し、辺の平行・垂直関係と長さの等しさを四つの多項式に変換した。証明したい「対角線が垂直」という結論も、多項式が0になるという形で表せる。すると、図形の証明は、前提の式を使って結論の式を消去できるかという計算になる。

中心となるのが「擬除算」だ。多項式の最高次の項を、乗算と減算を組み合わせて消していく。通常の割り算のように係数で割る操作を避けながら、式を小さくする手法である。今回の実験では四段階を経て、最後の余りに相当する多項式が0になることを確かめた。図形がつぶれないなど、手法に必要な条件の下で結論が導かれる。

量子回路に載せたのは、数式の文字列そのものではない。係数を表す多項式について、その形を一意に決められるだけの点で値を用意し、量子ビットのまとまりへ符号化した。この表現により、多項式の操作を点ごとの値の乗算・減算へ置き換えられる。

ただし、点の値は従来型のコンピューターで事前に計算され、量子回路へ埋め込まれている。量子プロセッサーが実行したのは、その値を使う擬除算の算術操作だ。測定で得た分布から各点の値を読み取り、途中の多項式を復元して次の段階へ進む。

ここでの「0」は、適当な正方形を何枚か描いて直角になった、という観察とは意味が違う。多項式を決めるために選んだ点と、代数的な消去手続きが証明を支えている。一方、実機の出力は雑音を含む測定結果であり、理想的な数式操作の妥当性と、その操作を装置がどれほど正しく実行したかは分けて評価する必要がある。

AD

IMO問題では角の関係をつなぐ

1978年IMO第4問は、二等辺三角形と円に関する問題だ。二等辺三角形ABCの等しい辺AB、ACに、それぞれF、Gで接し、さらに三角形の外接円に内側から接する円を考える。このとき、線分FGの中点Hが、三角形ABCの内心になることを示す。内心とは、三角形の内接円の中心である。

論文で扱う配置では、対称性からHは頂点Aの角を二等分する直線上にある。残る仕事は、Hを通る直線が頂点Bの角も二等分することを示すことだ。研究チームはこの条件を、直線から別の直線へ測る向き付きの角度で表した。この「有向角」の表現では、直線の向きを半回転させても同じものとして扱う。

量子回路には、次の操作を提案する戦略回路と、決められた変形を実行する推論回路を組み合わせた。さらに評価回路で、適用した操作が状態を変えたかを調べる。その測定結果を使い、古典計算側で戦略回路のパラメーターを調整する。許された規則を固定しているため、探索の途中で勝手な論理を持ち込む構成ではない。

実験に使う三つの角の等式は、あらかじめ前提から古典的に導き、推論回路へ直接組み込んだものだ。量子回路は、それらを選んで適用する処理を三ラウンド進め、目標の等式へ至った。問題文を読んで補助線や証明規則を自力で発見したわけではない。

論文の図3は、各1000回の測定を10回繰り返して得た分布を示す。各ラウンドで期待される操作と出力が最も強く現れ、その結果から証明の連鎖を再構成した。出力を測定した後、その代表的な結果を次の入力として準備し直す。複数段階を通じて量子状態を保ち続けた実験とは区別される。

量子回路と古典計算の分担を追う

二つの実験はいずれも古典計算による準備を伴うが、量子回路が担ったのは、正方形では多項式の演算、IMO問題では用意された関係式の選択と適用だった。

研究チームの2026年9月13日版論文について、代数的証明と記号的証明探索の各節、および結論の実装条件を、同じ工程ごとに並べると次のようになる。

工程 正方形の対角線 IMOの幾何問題
事前に用意するもの 多項式を表す点ごとの値を古典計算で求める 前提から導いた三つの角の等式を選び、回路へ組み込む
量子回路が実行するもの 擬除算に必要な乗算と減算 次の操作の提案、関係式の適用、変化の評価
段階間の受け渡し 測定結果から途中の多項式を復元する 出力を測定し、次の入力状態を準備し直す
到達した結果 四段階の消去で最後の多項式が0になる 三ラウンドで角の関係をつなぎ、内心の条件を示す

出典：主論文の実験記述と結論。同じ研究の処理分担を比較した表であり、二方式の速度や能力の優劣を示すものではない。

表から分かるのは、量子回路に推論の具体的な操作を担当させつつ、入力の準備と段階の接続には古典的な処理を残した設計である。研究の価値は、この分担の中で代数的な変形と記号的な選択の両方を実機に載せた点にある。証明全体を自律的に組み立てる汎用システムと評価するには、まだ条件が異なる。

装置の規模も分けて読む必要がある。121量子ビットはプロセッサー全体の数だ。補足資料の図S11に示す各回路の使用数は17から32量子ビットであり、全量子ビットを一つの証明に投入したわけではない。本文で具体的に説明された正方形の最初の回路も、21量子ビットを使う。装置に載っている数だけで、扱える証明の複雑さを判断することはできない。

AD

量子優位の検証はこれからだ

Sun氏らは2026年1月の先行研究で、量子自動定理証明の理論的な枠組みを提案していた。そこで示した利点の一つは「問い合わせ計算量」の二次の改善である。これは、問題が大きくなったときに必要な問い合わせ回数をどう減らせるかという議論であり、装置の処理時間が単純に二倍速くなるという意味ではない。

今回の実験論文も、呉の方法の量子実装について、理論上の優位性はまだ実証していないと明記している。回路の大きさと深さはハードウェアの誤差に制約される。さらに、実用的な速さを評価する際には、事前計算や回路の準備、繰り返し測定まで含めて考える必要がある。量子状態に多くの候補を載せられることだけから、証明全体の高速化は結論できない。

古典計算による幾何の自動証明は、すでに別の方向で進んでいる。2024年のNature論文で報告されたAlphaGeometryは、言語モデルによる補助線などの提案と記号推論を組み合わせ、オリンピック幾何のベンチマーク30問中25問を解いた。今回の二例とは問題の範囲も評価目的も違うため、その数字を並べて量子方式の勝敗を決めることはできない。問われているのは、既存AIを上回ったかよりも、証明の処理を量子計算へ移す実験がどこまで成立したかである。

著者らは、より大きな知識ベースや豊富な規則を扱い、途中の量子状態を次の推論へ直接渡す方向を展望している。実現には、より大規模で誤りの少ない回路が必要になる。論文ではデータと解析・数値シミュレーションコードを出版時にZenodoで公開する予定としており、第三者による再現性の検証も今後の判断材料だ。

既知の証明を量子回路で動かす段階から、候補の多い証明探索で利点を示す段階へ進めるか。前処理や測定を含む条件をそろえた比較と、段階をまたぐ量子状態の保持が実現すれば、量子計算が数学の推論に役立つ場面を具体的に見極められるようになる。