つづき

分野としては全然違う話ですが、昔、竹崎正道先生が東大に来た時に「Connes は超準解析を勉強しているから、
彼の仕事（多分、von Neumann 環の分類に関する話）には ultraproduct （だったかな）使いまくりですよ。普通の言葉で書き直そうと思えば出来ないことはないけれど、極限だらけになって何をやっているのか分からなくなる」という話をされていたのを思い出しました。
他に、数学セミナーで読んだモデル理論を使った代数幾何の話とか。もっとも、上の "univalent foundation" の話は「基礎論的な話の数学への応用」だけではなく、逆に型理論の方に homotopy 論的な見方を持ち込もうとしている所、計算機上の implementation も考えている所が特徴のようです。

Voevodsky 先生、ある新聞のインタビュー（ロシア語）では「Princeton は教えなくて良いから選んだ」と言っていたので、学生が嫌いなのかな、と思っていたら、質問（こっちの学生さんは誰に対しても活発にいろんなレベルの質問をする）に丁寧に答えていたので、認識を改めました。
話し方も楽しかった。最初のツカミはこんな感じ：「数学はどんどん複雑になってよく分からなくなって論文が間違っている可能性が増えてきた。そりゃそうで、一番面倒な所に間違いがある可能性が高いが、レフェリーが一番読まないのがそういう所だから。」同感。
（引用おわり）