この動画は2025年の国際数学オリンピックにおけるAIの参加について解説したものである。GoogleのDeepMindが公式に金メダルを獲得した一方で、OpenAIとByteDanceは自己申告での成績を発表した。特にByteDanceの新しいSeed-Proverモデルの3段階推論戦略や、数学的証明における自動化技術の進歩について詳しく分析している。
国際数学オリンピック2025におけるAIの挑戦
やあみんな、また戻ってきてくれてほんまに嬉しいわ。今日は不可能な数学の問題と、AIがそれをどう解決するかについて話していこうや。
みんなも知ってる通り、毎年国際数学オリンピックっていうのがあってな、2025年はオーストラリアのサンシャインコーストで開催されたんや。20歳未満の若い才能あふれる人たちが参加してな、島の住民たちに温かく迎えられて、もうほんまに素晴らしい大会やったんや。
でもな、実は3つのAI企業も参加することにしたんや。1つは完全に公式、1つは全く非公式、そしてもう1つはサプライズやった。これについて詳しく見ていこうや。
ここにIMOの会長の声明があるんやけど、「GoogleのDeepMindが待ち望まれていたマイルストーンに到達したことを確認できます。金メダルスコアを獲得しました。多くの面で驚異的で、評価も明確で正確、そしてほとんどが理解しやすい説明でした」って公式に発表されたんや。GoogleのDeepMind、金メダル獲得や。
技術的な面で興味深いのは、Googleが形式数学の構造から非形式数学の構造に切り替えたことなんや。つまり、IMOから与えられた自然言語の問題を領域特定言語に翻訳することから、Lean形式を選択したってことやな。
Googleは言うてるんや、「2024年は計算だけで2〜3日かかってたけど、2025年は金メダルを獲得できた。なぜなら我々のGeminiモデルが今や自然言語でエンドツーエンドで動作するようになって、通常の4時間半の競技時間制限内で競技できるようになったから」ってな。素晴らしいことやで。
でも彼らはこうも言ってるんや。「Geminiは今、新しい強化学習と事前学習での理論データストリームで訓練されてる」ってな。めちゃくちゃ興味深いやろ。
GoogleのAlpha Proofシステムの技術的詳細
今年は2つの選択肢があるって言ってるんや。自然言語ベースのアプローチを取る一方で、LLM用のLeanのような形式言語システムでも進歩を続けてるってことやな。これはAlpha GeometryとAlpha Proofって呼ばれてる。
Googleは言ってるんや、「自然言語の流暢さと、Leanのような形式言語での厳密な推論を組み合わせたエージェントが、数学、科学、工学研究、そしてあらゆる分野で非常に価値のあるツールになると信じてる」ってな。ほんまに魅力的やで。
Alpha Proofに馴染みがない人のために、簡単にまとめておこうか。
DSP 3の文脈でLean 4について話したのを覚えてるやろうけど、いつものようにLLMがあって、このLLMはエージェントとしてツール使用とメモリを持ってるんや。だからツール使用はLean 4になる可能性があって、何と美しい強化学習も推論時に並列で実行できるんや。
もう一つの選択肢もあるで。もしGoogleで10万個のGPUを持ってるなら、問題ないやろ。「ちょっと待てよ、LLMがあって、普通の英語言語学じゃなくて、今度はLeanのような形式言語、コンピュータ言語があるやんか」って言えるんや。
LLMは言語パターンを学ぶか形式言語のLean 4パターンを学ぶかなんて気にしないんや。だから彼らはLean 4の解法証明定理の巨大なデータセットを作成して、抽象的推論や証明プリミティブでこのLLMを訓練するのに使ったんや。
ほんまに魅力的やわ。たった2週間前のプリンストン大学のビデオで、彼らの超知能もシンボリック論理プリミティブに基づいて構築されてることを示したの覚えてるやろ。でもプリンストンは特定のタスクのために知識グラフから論理プリミティブを導出してるんや。Googleは今、もっと一般的なアプローチを取ってるんやで。
Alpha Geometry 2についてもっと学びたいなら、この論文を強くお勧めするわ。
OpenAIの非公式参加とその問題
でも言ったように、自分のシステムを十分信頼せずに公式参加しなかった非公式参加者がいたんや。どのAI企業か分かるやろ。
630人の人間の学生以外の2番目の非公式参加者について話そうや。結果を発表できるで。ここで発表されてるように、11%が金メダルを獲得したんや。
20歳未満の若い数学者の11%、つまり67人の競技者が金メダルを獲得したんや。そして1つの企業があったんやけど、私は検索アルゴリズムにChatGPTを使って、「OpenAIは2025年のオーストラリアでのIMO競技に公式参加したか？」って聞いたんや。
OpenAIのChatGPTは「いいえ、OpenAIは公式参加してません」って答えたんや。なぜならGoogleのDeepMindは正式に参加してIMO主催者と協力し、Googleの結果はIMOの審査員によって公式に評価され認定されたからやってな。
一方OpenAIは違うことをすることにしたんや。OpenAIは対照的に、一部の元人間メダリストを使って内部でモデルのパフォーマンスを評価したって言ってるんや。だからOpenAIに雇われてるってことやな。
OpenAIは特定の専門家を選んで、過去に金メダルを受賞した人たちを選んだんや。もちろんOpenAIはアメリカのビジネスモデルやから、これらの専門家にサービス料を支払ってるんやで。そして内部で評価して、OpenAIは公式に金メダルを獲得したと宣言したんや。
でもOpenAIは正式なIMOプロセスを通じて何も提出せず、公式競技エントリーリストの一部でもなかった。ChatGPTによって検証されたって読んだ時にな。
まとめるとこうやで。GoogleのDeepMindは公式に参加して、GoogleのDeepMindのパフォーマンスはIMO委員会によって認定された。OpenAIは公式参加しなかった。自分のシステムを十分信頼せず、公式プロセスを通らなかったけど、元IMOメダリストを雇って自己採点して、そしてOpenAIは金メダルの勝者だと自分で宣言したんや。結果発表の締切を守らなかったようで、みんなより先にやったんやで。
この企業はニュースやソーシャルメディアに出ることにとても熱心で、630人の学生全員に対して、推奨されない行動を示したんや。
ByteDanceのSeed-Proverシステム
でも今日見つけた他の企業について話そうや。何と、グローバルAI企業から別の競技者がいたんや。分かるやろ、中国やで。ByteDanceや。
彼らのモデルに馴染みがないかもしれんけど、Seed 1.5 Sinkingモデルを持ってるんや。彼ら自身は強化学習を使った先進的で優れた推論モデルって呼んでるんやで。
4日前にByteDanceのHugging Faceで全部見つけることができるわ。新しいアイデアと新しいモデルがあるんや。
でも昨日、私にとっては2025年7月31日に発表されたのが、「Seed-Prover: 自動定理証明のための深く広い推論」っていうのや。これが今回のビデオのメイン論文やないんやけど、「ちょっと待て、Googleも証明器を持ってて、それもファインチューニングされてて改善されてる」って言うかもしれんな。
今日学んだのは、何と中国のByteDanceもIMO証明器を持ってるってことや。Alpha Proverじゃなくて、Seed Proverって呼ばれてるんや。彼らのモデルがSeedって呼ばれてるからな。
でもこれはほんまに興味深い論文で、どうやって訓練したかについてもオープンにしてるんや。見ての通り、Seed Prover LLMとSeed Geometry LLMがあって、これはGoogleのAlpha Geometry 2やAlpha Proverとまったく同じアプローチやな。
中国が今言ってる非常に似たアプローチで、「俺たちもこれができるで」ってことやな。いろんなベンチマークがあるけど、見ての通り100%がトップラインで、Seed Proverは今このテストを飽和させて100%近くを達成してるんや。
ここでDeepSeek Prover バージョン2が見えるやろ。DeepSeek Prover バージョン2についてビデオを作ったことがあるけど、まだ90%以下やった。でも今、数ヶ月後には100%になってるんや。だから新しい何かが必要やな。
そして中国の人たちも言ってるんや、OpenAIの行動に従って、彼らもIMO 2025の6問中5問を成功裏に証明したって自己申告してるんやで。だから彼らも金メダルを獲得したってことや。これは私の解釈やけど、OpenAIが金メダルを自己申告したのとまったく同じやな。
ByteDanceは公式に招待されたって学んだんやけど、OpenAIが公式に招待されたかは確かじゃないな。でもByteDanceも言ってるんや、「でも承認の一つが締切後に終わった」ってな。だからIMO 2025の委員会によって公式に授与されなかった2つの金メダルについては、ちょっとした裏話を知っとくべきやと思うわ。
Seed-Proverの技術的アーキテクチャ
でもByteDanceの技術について話そうや。核となるアイデアは、問題を探索して、操作可能な中間ステップを生成・改善し、複雑さをより低い複雑さの補題に削減して数学的証明を行い、この証明と補題を構成要素として使って最終証明を構築することなんや。
いつも同じアイデアやってのが分かるやろ。AI分野全体で新しいアイデアなんてないんや。複雑さを削減して、プリミティブな構成要素に行って、それから構築するんや。
彼らは予算のための3段階推論戦略を設計したって言ってるんや。これは興味深いで。見てみようか。
数学での補題スタイルに馴染みがないなら、簡単に思い出させてもらうわ。彼らは「この補題スタイルは興味深くないけど、持ってる別の問題も解決しよう。それは継続学習や」って言ってるんや。
これらの補題がLean 4コンパイラによって証明されてるなら、補題プールを構築しようってことや。この補題プールは今、持続的で検証可能なコンパイラ知識プリミティブの形を表してるんや。
だからモデルは単にテキストを生成してるだけじゃないんや。信頼できるツールのライブラリを構築してるんやで。これは補題のことや。だからAPI呼び出しのあるツールじゃなくて、数学的に動作することが証明されてて、異なる試行で再利用できるソフトウェアパッケージのようなツールなんや。
このアイデアで達成したのは、数学レベルで知識を蓄積・複合化することや。彼らは狭いシンボリック相乗効果を構築し続けてるんや。だから補題はニューラルネットワーク部分で、創造的で直感的なステップを提案するのに優れてるんや。一方、シンボリック部分のLean 4コンパイラは即座の検証を提供するんや。だからほんまに強いフィードバックループがあるんやで。
一歩引いて強化学習として見てみると、Lean 4コンパイラが報酬モデルやってのがすぐ分かるやろ。これは単純に強化学習の演習なんや。でも数学的補題を蓄積してることを覚えといてな。
推論戦略を最適化するために、4時間半しかないから、日や週間動かすわけにはいかんのや。だから3段階干渉戦略、軽い、中程度、重い、を持ってるって言ってるんや。いつものように強化学習で達成したいのは、解決策の幅と深さのトレードオフなんや。だから再び探索と活用の最適化に直面してるんやで。
軽度推論設定の詳細
軽い推論設定を見てみようか。最初の全体証明があって、それをLeanコンパイラでチェックするんや。赤いXが見えたら動いてないってことや。だから何が起こったかを自己要約するんや。Lean 4から返ってくるエラーメッセージは何やった？多分証明の別バージョンを書き始めるかもしれん。
別のプロンプトをLeanコンパイラに再び入れるんや。ダメか。エラーメッセージを返してもらう。メモリがある。だから最適化された自己要約を書いて、自己修正しようとするんや。
そしてずっと続けて、Leanコンパイラが「おお、これは正しいやつや」って言ったら、解決策ができるんや。
中程度の推論設定に行くのはもうちょっと困難や。なぜか分かるか？補題ベースで構築されてるからや。だからLinkコンパイラが「見せてもらったプロンプトは動いてない」って言ったら、今通ったばかりの軽い干渉スキーマを各特定の補題に使うんや。
新しいコンテキストで問題があったら、これを再び通る。コンパイラからゴーをもらうまで内部精密化ステップがあるんや。
複雑さを他の方法の肩の上に構築してるのが分かるやろ。もちろんIMO25のような本当に興味深い問題では、重い推論設定に頼らなあかんのや。
でも補題アプローチやから、すぐに理解できるで。異なる推測があって、2分後に例を見せるわ。そして軽い推論で解決策を見つけようとするんや。時間を無駄にしたくないし、エネルギーも無駄にしたくない。うまくいくかもしれんし、いかんかもしれん。
問題に遭遇したら、中程度の干渉方法論に行くんや。これ全部を通って、5,000個まで推測できるって言ってるんや。例を見せるわ。
そしてすべての可能性を通すだけや。このSeed Prover、これについて話すと、非常に特定の戦略を持った非常に一般的なリストなんや。
重度推論設定での創造的アプローチ
まず、複雑さを分解して独立した再利用可能な補題に分解するように訓練されてることに注目や。まずLean 4で複雑さを削減して、これがLean 4での簡単なコードの例や。すぐ分かるやろ。補題アプローチで達成するのは、進捗追跡、モジュール性、再利用性、インスピレーション、補題の一般的証明が他の補題を提供するためのヒントを提供できることや。
プールにこれがあれば素晴らしいやん。軽い推論についてもうちょっと詳しく見てみようか。例をいくつか見せるって言ったやろ。
軽い推論の全体的な目標は何か？簡単な問題を解決して、構文的または軽微な推論エラーをすぐに修正することや。何をするか？簡単な精密化ループがあるんや。
言語モデルがLean 4で証明の試行を生成するんや。このコードはLean 4コンパイラに渡される。実行されて失敗したら、コンパイラが「すまん、エラーや」って言うんや。でも何が間違ってたかのフィードバックを提供するんや。
だからLLMはこの問題、失敗した試行、Lean 4エラーメッセージを入力として受け取って、失敗の自己要約と一緒に受け取るんや。だから何が間違ったかを理解しようとして、次にうまくいけばLean 4証明を書く正しい試行を生成するんや。
このループを8〜16回繰り返すことができて、これは非常に軽い複雑さだけのためやってのがすぐ分かるやろ。
中程度の推論や深い潜り込みに行く場合は、より複雑な部分問題に分解する必要がある複雑な問題を解決せなあかん。だからネストした精密化プロセスがあるんや。
これを見てみようか。外側の精密化ループと内側の精密化ループがあるんや。そしてそれは軽いループなんや。
外側の精密化ループは軽い設定のように主定理で動作するんや。だからこのループが有用な補題を生成するけど証明に失敗したら、内側の精密化ループをスポーンするんや。その一つの困難な補題を証明することだけを任務とする独自の専用予算を持った完全な軽い干渉プロセスや。
内側のループが成功したら、証明された補題が外側のループにフィードバックされて、主証明での作業を続けることができるんや。だから複雑さを下げて分割して、戻ってきて、今度は完全な複雑さがあるけど簡単になってるんや。
重い推論構造を見るのは本当に興味深いで。これは証明パスが完全に未知の最も困難な問題に取り組む場所なんや。進む道が未知の場合に何をしたいか考えてみてや。発明的である必要があるやろ。
100や1000のアイデアをチェックアウトして、そのアイデアの一つが進む道かもしれんって言うんや。これがまさにAIがすることなんや。
推測があって、今生成するんや。何かを証明しようとする代わりに、モデルは最初に与えられた特定の問題に関連する数千の潜在的に有用なアイデア推測を生成するようにプロンプトされるんや。だから問題空間を非常に広い方法で探索するんやで。
それからフィルタリングがある。システムは効率的な軽い推論を使うんや。補題アプローチで、数千の推測のそれぞれを自動的に証明または反証しようとするんや。ここで並列化が最重要やってのが分かるやろ。
それから補題プール集団になる。数千数千の契約者からの成功した証明された契約者すべてが今信頼できる補題になるんや。今特定のタグが隣についてて、「これは信頼できる。この特定の数学的証明を検証した」って言えるんや。そして問題の補題プールに追加されるんや。
だからシステムはクレイジーなアイデア、数千数千のアイデアを試すことで、次のレベルへの梯子を構築してるんや。そして最終的に何日もの思考の統合、本当に何日もの思考について書いてるんや。このプールを生成しなあかんからな。
システムは数百数千の非自明な証明された事実を数学的補題で蓄積してるんや。それから最も有望な補題を選択して、これを判断する異なる方法があって、中程度の推論設定を使って最終的に主定理の最終証明に織り込むんや。
だからループの中にループがあって、補題アプローチなんや。シンプルやけど、このアイデアに到達して、機械に「5,000の契約者を生成しろ。試してみろ。動くのが一つ見つかるかもしれん」って言う勇気が必要なんや。
ByteDanceの現在の技術的立ち位置
Google 2024は自然言語プロンプトを形式言語Lean 4プロンプトに翻訳するのに人間の介入があったって言ったやろ。今ByteDanceについて非常に興味があったんやけど、彼らはIMO 2025の見出しの下で人間翻訳について教えてくれてるんや。
彼らのAIは試験用紙から自然言語数学問題を読むことはない。代わりに、すべての問題は人間の専門家によって形式言語文に翻訳されたんやって。
だからこの特定のスライスで、ByteDanceは今Googleが2024年にいた場所にいるんや。人間の専門家が必要やったんや。Google 2025は既にシステムを純粋な自然言語処理の次のステップに切り替えてることを覚えといてな。
だからこの専門家は今英語の問題をLean形式の正確な定理文に変換したんや。もちろん人間のパフォーマンスが良いほど、AIにとって解決が簡単になるんやで。
彼らは「これは重要なステップや。自然言語理解はByteDanceの実装にとってまだ大きな課題やから」って言ってるけど、Googleがちょうど1年未満前にいた場所で今これができるんやで。
そしてAI証明がある。問題がLean 4で形式化されたら、Seed ProverとSeed Geometryシステムが引き継ぐんや。Googleと同じように、巨大な計算資源と論文で説明された方法、補題生成推論を使って、形式証明を作成するんや。
この証明はLean 4コードの完全な検証ブロックで、Lean 4コンパイラがあるんや。だから簡単な報酬システムと検証があって、どう続けるか分かるやろ。
Seed ProverとSeed Geometryの両方がLLMによって動いてて、これらのLLMはLean 4データ、Lean 4証明、コンパイラ相互作用で特別かつ集中的に訓練されたんや。だから再び、どこにいるか？完璧な批評LLMを使った強化学習にいるだけや。でも今は批評LLMじゃない。
今はLean 4コンパイラなんや。形式言語コンパイラや。だからバイナリ報酬信号を得るんや。イエスかノーか。アクション報酬は、重みを更新するのに使われる明確で曖昧でない訓練信号を提供するんや。素晴らしい外在的RLや。
そして思ったんや、「ちょっと待て、彼らは既にGoogleが今年いるステップにいるのか？Lean 4が今事前訓練データに統合されてて、Lean 4の論理を完全に本質的に学習してるのか？それとも推論実行があるときにまだLean 4をツールとして使ってるのか？」ってな。
論文を読んでるだけやけど、ここのワークフローを見てや。すべてのステップでLeanコンパイラを報酬信号の生成器として持ってるのが分かるやろ。Leanコンパイラが「これは赤いX、これは失敗や」って言ったら、ツールとして持ってるのが分かるんや。
だからByteDanceが今日発表したばかりのものとGoogleが2024年にしたこととの本当のデルタは何かって自問したんや。本当に興味深いと思うのは、3段階戦略アプローチを持ってることや。軽いシナリオでバグ修正で即座に解決可能なものを解決する。それから複雑さの次のステップ、中程度の問題、見せた補題での深い潜り込み。そして重いもので、パスが絶対に未知の時の探索的推測生成に本当に入らなあかん。
訓練データには何もない。どこにも何も利用できない。これは誰もそれについて知らない真新しい処女問題や。どこにも何も利用できない。だからAIとして創造的でなければならない。
Seed-Proverの戦略的思考レイヤー
このシステムは数学レベルで自己学習補題プールを自動的に作成するんや。だから持続的に成長するデータベース、多分データベースは間違った言葉かもしれんけど、非常に特定の問題のために証明された事実の成長する知識ベースで、Lean 4コンパイラに入力して緑のライトをもらえるかどうか分かるんや。
だからByteDanceはここで戦略的思考家のアプローチをこのブロックバージョンで実装してるんや。だから計画をスケッチして、契約者を提案して、必要な副結果や低複雑度補題を証明して、それから最終議論を組み立て始めるんや。
だからSeed Prover、今の私の簡単な解釈やけど、もし間違ってたらコメントに何か残してくれ、このSeed Proverは今ループの上に戦略的レイヤーを追加してるんや。
「次のコード行は何か？」って聞くだけじゃなくて、次のレベルの質問をするんや。「この問題は直接解決するのに十分簡単か？軽い推論。この一つの補題で行き詰まってる。そこにすべてのエネルギーを集中しよう。中程度の推論。または何をすべきか全く分からない。重い推論。」
だからズームアウトして、非常に特定の方法で中間目標を管理・作成・設計しようとするんや。だから証明された補題と証明されてない推測があって、計算資源をどう動的に割り当てるか。これがSeed Proverが本当に特別やと思うところで、これがSeed Proverについて読んだ最初の日やってのを覚えといてな。ByteDance自体のドキュメンテーション以外に他の情報は持ってない。だからこれが私の最初の理解なんや。
推測について追加情報を与えたかったんやけど、推測は証明されてない数学的文として見てるんや。推測や仮説、他の何でもいいけど役に立つんや。多分前進するステップかもしれん。だからその目的は巨大な問題空間全体をマッピングすることなんや。
これらの推測は暗闇に撃つ矢のようなもんや。または懐中電灯を持ってて部屋のあらゆる方向を指してるようなもんや。だから本当に一つにコミットすることなく、推論シーケンスで可能な限り多くの前進パスを生成または発見したいんや。
彼らはここでアーティストについて書いてるんや。システムはデフォルトで5,000の契約者という膨大な数を生成して、問題の興味深い特性をここでカバーすることを確実にするんや。だから完全な解決空間が少なくともベクトルバンドルか、懐中電灯のビームで角々に光を当てることで多かれ少なかれカバーされることを本当に確実にするんや。
考えてみてや。推測1は問題を与えられたとするやろ。そして推測1はLLMが「たぶん関数fは常に正か、関数は常に負か、関数は正と負の間で変動してる」って言うかもしれん。何でも推測2548になり得るんや。
「この三角形APCは特定の形状を持ってるか、特定の対称性を持ってる」って賭けるんや。これらは巨大な推測プールに浮かんでる数千数千のアイデアなんや。
それからフィルタリング段階に来るんや。システムは効率的な軽い推論設定を高速連射証明試行エンジンとして使うんや。各推測を一つずつ取って証明しようとするんや。失敗。成功。成功。素晴らしい。だから正のサンプルで信頼できる補題証明、信頼できる補題証明を集積するんや。
この過程を何日も経た後、数百または数千の非自明な証明された論理構造を含む補題プールができるんや。そしてシステムは歯車を切り替えるんや。今度は中程度の推論設定を使うんや。
これについてちょうど話したばかりやったな。それから重い推論設定に行くんや。でも今、中国の同僚が何をしたかを理解するビルディングブロックができたと思うわ。非常に興味深いで。
さらに、彼らがLean 4への独自の高性能インターフェースを構築したことも言及したいんや。Lu Kangっていうカスタム高同時実行Python インターフェースって呼んでるんや。興味深いな。
さらにジオメトリエンジンについて、話してないけど何かは推測できるやろ。彼らはSeed Geometryのシンボリック演繹エンジンをPythonからC++に書き直して、C++実装で100倍の速度向上を得たんや。
素晴らしいな。エラー修正のための自己要約。だからエラーメッセージを返すだけじゃなくて、プロンプトには今、異なる視点からの前回の試行の自己分析、自己要約が含まれるんや。メタ認知の形で、この特定の解決パスがなぜ失敗したかをモデルに反映させて、うまくいけばより知的な後続の試行につながるんやで。
最後に、補題選択のためのLLM審査員や。補題は承認された難易度だけでなく、意味的関連性によってもランク付けされるんや。もちろん意味的関連性は常に別の巨大なLLMによって判断されるのは知ってるやろ。
だから興味深いことに、パイプラインにこんなに多くのLLMがあって、その相互依存性があって、IMO 2025のこんなに多くの問題を正しく解くことができたんや。
これは、LLMが生成器としてだけでなく、評価器として、キュレーターとして、完全にもっと複雑な推論プロセス内でのアイデア提供者として使用される本当に洗練されたパイプラインやってことを示してるんや。だから興味深いな。
これは国際数学オリンピック2025への非常に短い旅やったけど、グローバル企業が何に取り組んでるかが分かるやろ。
「お金？お金なんてどうでもいい。1万や10万のGPU構成なんてどうでもいい。この地球上で持てる最大パワーで問題を解決したいだけや」って言ったらどうなる？そして3つの企業が成功したんや。
1つは公式で、これはGeminiモデルでのGoogleや。そして2つは自己申告でそのパフォーマンスを持ってたと宣言した。1つはアメリカのOpenAI、もう1つは中国のByteDanceや。
AI研究の最先端と出血の端を見るのは非常に興味深いな。楽しんでもらえたと思うわ。論文を見てみて、もし購読してくれたら次回会おうや。
コメント