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: |

Telegram boasts 500 million users, who share information individually and in groups in relative security. But Telegram's use as a one-way broadcast channel — which followers can join but not reply to — means content from inauthentic accounts can easily reach large, captive and eager audiences. Ukrainian President Volodymyr Zelensky said in a video message on Tuesday that Ukrainian forces "destroy the invaders wherever we can." Stocks closed in the red Friday as investors weighed upbeat remarks from Russian President Vladimir Putin about diplomatic discussions with Ukraine against a weaker-than-expected print on U.S. consumer sentiment. On February 27th, Durov posted that Channels were becoming a source of unverified information and that the company lacks the ability to check on their veracity. He urged users to be mistrustful of the things shared on Channels, and initially threatened to block the feature in the countries involved for the length of the war, saying that he didn’t want Telegram to be used to aggravate conflict or incite ethnic hatred. He did, however, walk back this plan when it became clear that they had also become a vital communications tool for Ukrainian officials and citizens to help coordinate their resistance and evacuations. "Markets were cheering this economic recovery and return to strong economic growth, but the cheers will turn to tears if the inflation outbreak pushes businesses and consumers to the brink of recession," he added.
from kr


Telegram Metaprogramming
FROM American