Наблюдаю, как массово репощут какие-то глупенькие посты, что дескать, смотрите, аж целый филдсовский лауреат (это как нобелевка, только в математике) Terence Tao пишет код с помощью жпт, и у него всё отлично получается. И какие-то мутные скриншоты "в подтверждение", которые на самом деле из его видео "Formalizing a proof in Lean using Github Copilot only", где уже само название как бы намекает, что "это другое". Вот тут код с его стрима: Lean formalization of asymptotic estimates

Тао занимается этим уже давно, в частности, в рамках фонда "AI for Math fund" разрабатывает AI-модели для автоматической формализации доказательств (ну, да, вайб-кодинг, но на функциональном языке Lean с завтипчиками) и генерации тактик для пруф-ассистантов, включая метаматематические подходы, и вообще очень активно занимается развитием Lean. Тао также создаёт интерактивные учебники -- как детализировать доказательства "до аксиом" через Lean, и т.п.
Почитайте его блог, увлекательно.

Одна из мечт Тао -- перевод математики с уровня "ремесленников" на "промышленные рельсы", чтобы стали массово доступными пруверы, способные параллельно доказывать сотни, тысячи теорем. Фишка в том, чтобы разные участники проекта могли сфокусироваться на узких задачах (например, формализации лемм), а не на понимании всей теории, а "тимлид" аккуратно бы этим процессом руководил.

Трудится Тао на гранты Национального научного фонда США, техногигантов уровня Гугла, заинтересованных в ликвидации всех программистов формальной верификации кода, а также увы увы ряда откровенно недружественных структур.
Одна из тем его исследований например -- компрессионное зондирование (compressive sensing - восстанавливаем сигнал по его истории), актуальное для радиоэлектронной разведки, взлома спецсигналов номерных радиостанций...

Но, думаю, на 80-90% его деятельность публичная, за что ему дикое уважение.

У нас, вот конкретно что по темке Lean или Coq по профилю Тао? Какие-то фрагментарные исследования, единичные энтузиасты, в основном чистые математики, существенное отставание от США, нулевое финансирование, тотальная утечка кадров... Ни блогов на русском, ни гитхабов. Какие-то полудохлые чатики в тг, где одна вода, и всё.

При том, что любимая Российская Федерация и по сей день отличается сильнейшей в мире абстрактной математикой благодаря глубоким традициям математической логики (Школы Колмогорова, Лаврентьева, Маркова...).

=

Я кстати в сентябре 24-го думал "запилить hott-плагин для Lean", но у меня старенький комп особо не тянет Lean даже без AI :)
Вот тут: "Термы -- это деревья, а деревья -- это термы"
А для задач уровня Тео надо уметь перемалывать/переписывать десятки, сотни миллионов термов.
Мои тогдашние оценки:
"...vds с озу 200 гиг под подобные задачки стоит дороже, чем дедик, меньше $100/месяц не получается...
Рабочие станции Dell 7920, HP Z8 G4, Lenovo P920 (потенциально терабайты оперативки) продаются с 16 гб (!) от трёх тысяч долларов (а серваки уже от $5 тыс)."

=

Ладно, всё равно никому это не нужно. Доделываю курсы по базовой теории HoTT на Lean питончике (на которые впишутся два с половиной курсанта, но и этот будет хороший результат), потом подетальнее поизучаю, что такого Тао делает в плане обучения формальным подходам, и попробую его идеи как-то отмаппить на топологически-ориентированное проектирование. А вдруг?