Поизучал ночку блоги филдсовского лауреата Terence Tao, его научные труды, стримы с вайб-кодингом на Lean, повспоминал других аналогичных топовых пацанов в теме,
за которыми слежу не один десяток лет, и вот что могу вам сказать, дорогие:

Математика существенно проще, чем программирование.

Даже на уровне миддлов. Сеньор с хорошим образованием в информатике вообще без проблем впишется в ряд cчитающихся сложными математических тем, но даже продвинутый PhD будет сильно страдать на джуниорском уровне.

Это не программисту надо знать математику, а математику надо знать программирование.

Когда я делал реализацию HoTT, местами регулярно удивлялся, ну это же в принципе вещи достаточно простые. Ладно, видно я просто чего-то не понимаю....

Пока на блоге Тао не словил инсайты.

=

Тео регулярно хайпует упоминает проект формализации гипотезы Polynomial Freiman-Ruzsa (актуально в частности для криптографии: анализ псевдослучайных генераторов), доказательство которой было декомпозировано АЖ на 512 лемм, каждая из которых проверялась в Lean независимо.

Думаю, что многие из вас посмеются. 500 лемм считай -- это 500 функций/классов, пусть даже с хорошими спецификациями с TDD, с пред- и пост-условиями после BDD. Это просто уровень крепкого миддла.

Причём это не притянуто за уши, это реально глубокая аналогия.

Доказательство лемм и проектирование функций -- это две стороны одной медали: строгое управление сложностью через формальные спецификации. Это вполне можно назвать изоморфизмом (ну ладно, слабым: имеем глубокое структурное подобие без абсолютной тождественности). Это как два разных языка, описывающих одни и те же логические закономерности, но с собственной грамматикой и нюансами.

Тао сам говорит:
Математическое доказательство и программная абстракция - два языка описания логических структур...
Математическое доказательство - это предельный случай строгой спецификации...
Программирование - частный случай математической абстракции...

И вот дальше начинается САМОЕ интересное и важное....

продолжение следует