Warning: mkdir(): No space left on device in /var/www/group-telegram/post.php on line 37

Warning: file_put_contents(aCache/aDaily/post/metaprogramming/-364-365-): Failed to open stream: No such file or directory in /var/www/group-telegram/post.php on line 50
Metaprogramming | Telegram Webview: metaprogramming/364 -
Telegram Group & Telegram Channel
Telegram Group » Hong Kong » Metaprogramming » Telegram Webview » Post 364
Metaprogramming
Kevin Buzzard — евангелист языка программирования (и формального доказательства математических теорем) Lean.

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

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

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

Манеру устных презентаций также можно оценить по многочисленным видео. Смешные штаны (инвариант), рубленные кричащие реплики (и по содержанию: слоганы), общие манеры... невольно, при всём уважении к заслугам выпускника Кембриджа в теории чисел, на ум приходят аэропортовые таксисты, чуть не хватающие мимо проходящих людей за рукав :)
www.group-telegram.com/hk/metaprogramming.com/364
644 views



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

"And that set off kind of a battle royale for control of the platform that Durov eventually lost," said Nathalie Maréchal of the Washington advocacy group Ranking Digital Rights. The S&P 500 fell 1.3% to 4,204.36, and the Dow Jones Industrial Average was down 0.7% to 32,943.33. The Dow posted a fifth straight weekly loss — its longest losing streak since 2019. The Nasdaq Composite tumbled 2.2% to 12,843.81. Though all three indexes opened in the green, stocks took a turn after a new report showed U.S. consumer sentiment deteriorated more than expected in early March as consumers' inflation expectations soared to the highest since 1981. READ MORE The regulator took order for the search and seizure operation from Judge Purushottam B Jadhav, Sebi Special Judge / Additional Sessions Judge. But Telegram says people want to keep their chat history when they get a new phone, and they like having a data backup that will sync their chats across multiple devices. And that is why they let people choose whether they want their messages to be encrypted or not. When not turned on, though, chats are stored on Telegram's services, which are scattered throughout the world. But it has "disclosed 0 bytes of user data to third parties, including governments," Telegram states on its website.
from hk



Warning: filemtime(): stat failed for aCache/aDaily/post/metaprogramming/-364-365- in /var/www/group-telegram/post.php on line 310

Warning: filemtime(): stat failed for aCache/aDaily/post/metaprogramming/-364-365- in /var/www/group-telegram/post.php on line 311

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

 Metaprogramming TG
Webview: 364
Metaprogramming.Telegram Webview
Metaprogramming Telegram TG Channel
Telegram Updated:
Telegram Metaprogramming
FROM American