Telegram Group & Telegram Channel
Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean.

Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.

Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:

— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!

Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)



group-telegram.com/metaprogramming/364
Create:
Last Update:

Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean.

Слайд из по-видимому знаковой презентации, процитированной в статье о данном математике в Вики.

Уровень аргументации математика первого ранга, логические цепочки утверждений и в целом связность речи поражает:

— Lean лучше, чем Coq (язык-конкурент — прим.)
— А чем лучше-то?
— Да чем Coq!

Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)

BY Metaprogramming





Share with your friend now:
group-telegram.com/metaprogramming/364

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

The Russian invasion of Ukraine has been a driving force in markets for the past few weeks. Ukrainian forces have since put up a strong resistance to the Russian troops amid the war that has left hundreds of Ukrainian civilians, including children, dead, according to the United Nations. Ukrainian and international officials have accused Russia of targeting civilian populations with shelling and bombardments. Some people used the platform to organize ahead of the storming of the U.S. Capitol in January 2021, and last month Senator Mark Warner sent a letter to Durov urging him to curb Russian information operations on Telegram. In 2018, Russia banned Telegram although it reversed the prohibition two years later. Although some channels have been removed, the curation process is considered opaque and insufficient by analysts.
from de


Telegram Metaprogramming
FROM American