Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean.
Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.
Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:
— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!
Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)
Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.
Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:
— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!
Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)
👍9🔥4
tgoop.com/metaprogramming/365
Create:
Last Update:
Last Update:
Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean.
Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.
Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:
— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!
Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)
Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.
Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:
— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!
Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)
BY Metaprogramming
Share with your friend now:
tgoop.com/metaprogramming/365