Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean. Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики. Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает: — Lean лучше, чем Coq (язык-конкурент — прим.) — А чем лучше-то? — Да чем Coq! Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)