Kevin Buzzard Lean
ケヴィン・バザード（Kevin Buzzard）とLean（リーン）の登場は、数学界における「ボエボドスキー以降」の最も熱いムーブメントです。ボエボドスキーが「理論的基礎（OS）」を作ったとすれば、バザードはそれを「実用的なムーブメント（アプリ開発）」へ変えた人物と言えます。
1. ケヴィン・バザード：数学界の「伝道師」
バザードは、もともと数論幾何学（ラングランズ予想など）のトップ研究者（インペリアル・カレッジ・ロンドン教授）でした。
- 転向のきっかけ: 現代数学の証明があまりに巨大化し、査読者が内容を完全に理解できず、「おそらく正しいだろう」という信頼関係だけで論文が受理されている現状に危機感を抱きました。
- 活動: 彼は「数年以内に、コンピュータで検証されていない数学論文はゴミ箱行きになる」と極端な予言をし、学部生を巻き込んで数学の定理を片っ端からLeanに入力するプロジェクトを始めました。
2. 証明アシスタント「Lean」とは何か
Microsoft Researchが開発したプログラミング言語・証明支援システムです。
- 特徴: 他のシステム（CoqやAgda）に比べて、「普通の数学者の直感」に近い書き方ができるように設計されています。
- ライブラリ
mathlib: 世界中の有志が、集合論からスキーム論、複素解析まで、現代数学の標準的な知識をLeanのコードとして蓄積している「数学のWikipedia」のような巨大なレポジトリです。
3. リキッド・テンソル複体（LTC）の検証
バザードとLeanが世界を驚かせたのは、2021年の「挑戦状」への回答でした。
フィールズ賞受賞者ピーター・ショルツが、「自分の最新の定理（リキッド・ベクトル空間に関する重要な補題）が、あまりに複雑すぎて自分でも自信がない。誰かLeanで検証してくれ」とネット上で呼びかけたのです。
- 結果: バザード率いるチームが半年かけてこれを完遂。ショルツは「これで夜も安心して眠れる」と語りました。
- 意義: 「現役のトップランナーが書く、最先端の難解な数学」がコンピュータで検証可能であることを証明した歴史的な瞬間でした。
4. Leanでの「証明」はどんな見た目か
数学者は紙に日本語や英語で書く代わりに、**「タクティック（戦術）」**と呼ばれるコマンドを入力します。
例:
intro n: 「nという任意の数があるとする」induction n: 「n についての数学的帰納法を使う」ring: 「これは環の公理から計算すれば自明だ」
コンピュータ側は、ユーザーが一行書くたびに「現在の前提条件」と「残されたゴール（証明すべきこと）」をリアルタイムで表示します。これは、数学の証明というよりは、「パズルゲームの攻略」に近い感覚です。
バザードたちは現在、「コホモロジー理論」の体系的な形式化に挑んでいます。
Leanの世界では「異なるコホモロジー論を同じ構造（型）として統一的に定義する」というプログラミング的な作業として具現化されています。