つづき
Johan Commelin(Utrecht)
加藤教授からお話がありました通り、アダム・トパーズ氏と私は「Liquid Tensor Experiment」を主導して参りました。このプロジェクトが成功裏に完了した後、多くの人たちから「Leanを用いてIUT理論を検証すべきではないか」という問いを投げかけられました。
その際の私の答えは一貫して、「日本の数学コミュニティの人たち、すなわちIUT理論の専門知識を持つ人たちが関与してくれる場合に限る」というものでした。ですから、加藤教授からLANAプロジェクト立ち上げの提案をもらったときの私の興奮は、皆様にも想像していただけるかと思います

Adam Topaz(Alberta)
私は数学者の中でも、少し特殊な立場にあります。私の研究は、本プロジェクトの両側面—すなわち「遠アーベル幾何学」と、Leanを用いた「形式検証」—の両方にまたがっているからです。この双方に真摯に取り組んできた者として、形式化がいかに数学的思考のあり方を変容させるかを、身をもって経験してきました。これこそが、本プロジェクトが存在する意義の核心であると私は信じています
数学は何千年も同じ手法で行われてきました。私たちは議論を自然言語で記述し、同僚と共有し、それが正しいかどうかを判断してきました。しかし、形式化は私たちにそれ以上のことを求めます。完全な明示性と正確性を強いるだけでなく、私たちが用いる数学的概念を根本から再考し、最適化することも求めてくるのです。形式化のプロセスには、依然として人間の努力と創造性が不可欠です。証明支援系が担うのは、論理的整合性のチェックです。定義や主張が正しく形式化されているかどうかを判断できるのは、依然として人間の数学者だけなのです

Kiran Kedlaya(USCD)
私は数学の形式化に関しては新参者ですが、IUT理論への関心はLANAプロジェクトの前からの長い歴史があります。2015年、オックスフォード大学で開催されたワークショップにおいて、IUT理論に馴染みのなかった多くの数論幾何学者が、望月教授による初期の論文の読解・発表を通じ、この主題を消化しようと一致団結したことがありました。そのワークショップでは、IUT理論に対するコミュニティの理解における突破口を開くには至りませんでしたが、多くの啓示を得る結果となりました

星裕一郎：数理研
残念ながら、私はまだ自分の役割を完全には果たせていないとも考えています。特に、先に述べた定理3.11から系3.12を導く論理について、LANAプロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じていること、その事実を私は重く受け止めなければいけません。そして、そのような状況に対して、自分自身の至らなさも強く感じています。
それでも私は、この1年以上の積み重ねが無意味だったとはまったく思いません。むしろ、ここまで真剣に考え、議論し、理解しようとしてきたからこそ、どこにその本当の難しさがあるのかが、以前よりもはるかに明確になったのだと思います。そのような意味においても、このプロジェクトで積み重ねてきた営みには、確かな価値と意義があると考えています。
最後に、ZEN数学センターおよび加藤文元教授に対して、深く感謝を申し上げます。これまでの様々な多大な支援と尽力なくしては、この有意義な活動は決してあり得なかった、そのことは疑いようのない事実です。本当にありがとうございます
(引用終り)以上