自動形式化（AIが数学を証明の言葉に訳すこと）とは？

数学で「定理」とは、正しいと証明されたことがらです。証明は、ふつう人の言葉と数式で書かれ、ほかの数学者が読んで確かめます。でも人の言葉には、あいまいな所や、「明らか」として省いた所があり、長い証明では見落としも起きます。

形式の言葉（形式言語）は、使ってよい記号と、そのつなぎ方の決まりが、すべてはっきり決めてある言葉です。数学をこの言葉で書き直すことを、形式化と呼びます。Lean（リーン）や Isabelle（イザベル）は、形式の言葉で書いた証明を、コンピューターに確かめさせる道具です（証明支援系と呼びます）。証明の一歩ずつが決まりに合っているかを確かめ、合わない所があると通しません。Lean では、この確かめを、核（カーネル）と呼ぶ小さな部分が受け持ちます。核は関所の番人のようなもので、どの証明も最後はここを通り、決まりに合わない一歩があれば止められます。Lean には、定義や定理を集めた Mathlib という、100万行を超える大きな数学の書庫もあります。

形式の言葉で確かめた証明は、正しさがほぼ完全に確かになります。四色定理（地図は4色あれば、となり合う国を別の色に塗り分けられる）のような、とても長い証明も、形式化されてきました。

AIの証明を確かめるのにも役立ちます。大規模言語モデルは数学の問題も解くようになりましたが、もっともらしいまちがい（ハルシネーション）をすることがあります。AIが人の言葉で書いた長い証明を、人が全部読んで確かめるのは大変です。証明の言葉で書かせれば、手順のまちがいは Lean が見つけます。

人の手でも訳せますが、とても手間がかかります。大きな証明の形式化は、ふつう専門家が何年もかけて、こつこつ進める仕事です。訳すには、数学の意味が分かることと、形式の言葉の細かい決まりを知っていることの、両方が要ります。

そのため、形式の言葉で書かれた数学は、人の言葉で書かれた数学に比べて、とても少ないままです。2022年の論文（Wu ほか）は、Isabelle の証明を集めた書庫（Archive of Formal Proofs）が約180MBで、AI（Codex）が学んだデータの0.18%にも足りないこと、同じ数学を人の言葉と形式の言葉の両方で書いた組は、ほとんど無いことを挙げています。2025年の AlphaProof の論文（Google DeepMind）も、人が Lean に形式化した問題の数は、人の言葉の問題より何けたも少ない、と書いています。

そこで、大規模言語モデル（LLM）に訳させれば、形式化の重い手間を減らせるのではないか、と考えられました。これが自動形式化です。

2022年の論文（Wu ほか）は、大規模言語モデルに、アメリカの中学・高校生の数学の競技（AMC・AIME など）の問題を集めた問題集（MATH）の問題を、Isabelle（イザベル。証明を確かめるソフト）の言葉に訳させました。訳し方を特別に学ばせてはおらず、お手本の訳を少し見せただけです。人が150問の訳を1問ずつ確かめると、AIの1つ（Codex）が完全に正しく訳せたのは38問、25.3%でした。

まちがいの多くは、人の言葉の意味と、形式の言葉の定義が、うまく合わないことから起きていました。たとえば、問題の「いちばん大きい値」を、Isabelle で決まっている書き方（Greatest や Max）で書けず、訳した文が「いちばん大きい」を正しく表せないことが、よくありました。「f は1次関数」という問題で、Isabelle に無い linear という言葉を、あるものとして作って書いてしまい、1次関数という条件を正しく訳せなかった例もあります。

その後、訳は正しくなってきました。2025年に論文が出た AlphaProof（Google DeepMind）の、訳す役のAI（Gemini をもとに作ったもの）は、国際数学オリンピック（IMO）の代表的な問題50問で、1問に1つだけ出した訳の60%が、正しい訳と評価されました。ただ、問題も言葉も確かめ方もちがうので、25.3%と60%を、そのまま比べることはできません。

Lean や Isabelle は、訳した文が形式の言葉の決まりに合っているか（文の形が正しいか）は確かめます。でも、元の問題と同じ意味かは確かめません。意味のまちがいを見つけるには、別の確かめが要ります。いちばん確かなのは、両方の言葉が分かる人が読むことです。でも、人の手では、たくさんは確かめられません。

そこで、AIに確かめさせる工夫があります。2024年の Lean Workbook という研究（Ying ほか）は、AIが訳した Lean の文を、AIに人の言葉へ訳し戻させ、元の問題と同じことを言っているかを、別のAIに判断させました。Lean で通らない文は除き、ちがうと判断された文は、人が直す方へ回します。こうして両方の確かめを通った約5万7千問の問題集から選んだ問題を、専門家が確かめると、93.5%が正しい訳でした。

この研究は、よく起きたまちがいも挙げています。Lean では、数の種類を書かずに 1/3 と書くと、整数どうしの割り算として計算し、答えの小数を切り捨てて0にします。小数も入る数として計算させるには、式の中に (1:ℝ)/3 と書き、「この1は ℝ（実数。小数も入る数）」と決めます。AIが式の中に、それを書かずに 1/3 と書いて、元とちがう式になってしまうまちがいが、くり返し見つかりました。

前から決めてある文と比べるやり方もあります。2026年9月に Anthropic（AIの会社）が発表した、AIによるフェルマーの最終定理の証明の形式化では、AIが証明した最後の文が、Mathlib にもとからあるこの定理の文と同じであることを、道具で確かめたとしています（会社の発表）。

証明を作るAIを鍛える、練習の問題としてなら、役に立ちます。2022年の論文（Wu ほか）は、MATH の練習用の問題3,908問をAI（Codex）に Isabelle の言葉へ訳させ、文の形が正しかった3,363問を使って、証明を作るAI（Thor）に、証明を探す練習をくり返させました。すると、miniF2F（数学オリンピックなどの問題488問を、人が形式の言葉に訳した問題集）の試験の問題で、証明できた割合が29.9%から35.2%に上がりました。それまでの最も高い成績（29.6%）を超えています。

Google DeepMind の AlphaProof（2024年に発表、2025年に論文）は、これをずっと大きくしました。人が Lean に訳した約2,500問を最初の材料にして、訳す役のAIを学ばせ、そのAIが、人の言葉の問題約100万問を、約8000万問の Lean の問題に訳しました。1つの問題から何通りもの訳を作ったのは、その中に正しい訳が入りやすくするためです。そして、強化学習（うまくできたらごほうびを与えて学ばせるやり方）で、証明の練習をさせました。論文は、訳したどの文も、元の問題に忠実かどうかにかかわらず、証明する（正しいと示す）か、反証する（まちがいだと示す）かを試せる、きちんとした形式の問題なので、練習の材料として役立つ、と書いています。まちがった訳は、練習の中ですぐに片づくことが多く、それ自体がおもしろい問題になることもあった、とも書いています。

ただし、元の問題を解いたと言うためには、訳が正しくなければなりません。練習の問題と、答えを出したい問題とでは、訳のまちがいの重さがちがうのです。