リヨンからパリへ向かう最近の列車の旅で、 ウラジーミル・ヴォエヴォドスキー は スティーブ・オーボディ の隣に座り、数学の進め方を変えるよう説得しようとした。
48歳のヴォエヴォドスキーは、ニュージャージー州プリンストンにある高等研究所（IAS）の常勤教員である。モスクワ生まれだが、ほぼ完璧な英語を話し、自分を誰かに証明する必要のない人物のような自信に満ちた風格を備えている。2002年には、数学界で最も権威ある賞とされることの多いフィールズ賞を受賞した。
列車が市内に近づくと、ヴォエヴォドスキーはノートパソコンを取り出し、数学者が数学的な論証を書くための環境を提供する証明支援系プログラム、Coqを起動した。ペンシルベニア州ピッツバーグのカーネギーメロン大学で数学者および論理学者を務めるオーボディが見守るなか、ヴォエヴォドスキーは自ら考案した新しい形式体系を使って数学的対象の定義を書いた。その形式体系は 一価基礎論と呼ばれる。ヴォエヴォドスキーがその定義を書くのにかかった時間は15分だった。
「私は［オーボディに］［自分の数学をCoqで行う］よう説得しようとしていた」と、ヴォエヴォドスキーは昨秋の講演で説明した。「それが簡単だと彼に納得させようとしていたのです。」
この記事の続きは、 Quanta Magazineをご覧ください。記事の掲載は、世界経済フォーラムがその見解を支持することを意味するものではありません。
アジェンダの最新情報を受け取るには、 週刊ニュースレターにご登録ください。
著者：ケビン・ハートネット。ケビンはボストン・グローブ紙「Ideas」欄で「Brainiac」コラムを執筆している。
画像：コンピューターのキーボードの「End」キー。REUTERS/Kacper Pempel。
