自然言語の曖昧な指示からコードを生成する vibe coding とは異なり、形式仕様に基づいて厳密に検証されたコードと証明を生成する vericoding が注目されています。本稿は、特定の数学の問題（IMO 1963 P5: 国際数学オリンピック1963年の第5問）について、最先端の汎用大規模言語モデル（LLM、GPT-5）と汎用コーディングAIエージェント（Cursor）を用いた、定理証明支援系 Lean による形式証明を生成した実践報告です。
ソフトウェアのバグは深刻な結果を引き起こしうるため、コードの正しさを数学的に証明する形式検証の重要性が増しています。しかし、その実施には多大な労力が必要でした。