Относительно мышления на условном уровне проектирования/ programming in large, всё что Terence Tao упоминает -- это сплошные эвристики. В проекте Lean4-Analysis-Tao Тао много занимался глубокой медитацией мысленными экспериментами-"симуляциями", чтобы определить, какие леммы нужны для доказательства сходимости рядов. По его словам, он мысленно проигрывал в голове возможные пути доказательства, выделяя ключевые шаги.

(Попробуйте-ка попросить своего менеджера выделить вам время на обдумывание структуры проекта -- в виде например "гулять по парку" или "сидеть в уличном кафе в медитации за чашечкой кофэ" :)

Интересно что Тао использовал подходы к декомпозиции, характерные сегодня для нейросеток: "Decompose-ToM: Enhancing Theory of Mind Reasoning in Large Language Models through Simulation and Task Decomposition"

=

И снова и снова Тао повторяет мантру, что процесс выделения лемм — это искусство, а не алгоритм. Дескать,
- контекстная зависимость
- нет универсальных правил для выбора лемм
- математик часто опирается на неявные знания и аналогии, которые сложно выразить в виде формальных шагов
- cлишком мелкие леммы усложняют общую структуру, слишком крупные - теряют ценность для повторного использования.

Тао подчеркивает, что декомпозиция — это не столько технический метод, сколь "думательная/мыслительная дисциплина". Он рекомендует применять SOLID
- начинать с простых аналогий (например, разбить доказательство теоремы Пифагора на 3-4 леммы);
- использовать пруф-ассистенты вроде Lean для визуализации связей между леммами;
- избегать чрезмерной детализации: леммы должны быть достаточно общими для повторного использования.
Лемма должна решать одну конкретную подзадачу, которая повторяется или критически важна для доказательства (SRP).
Леммы формулируются так, чтобы их можно было применять в разных контекстах.
Если промежуточная теорема требует многошагового доказательства, её разбивают на леммы. И т.д.

Ничего не напоминает? :)

Леммы — "библиотечные функции": однажды доказанные, они применяются в новых теоремах. Функции легко и просто вызываются в разных контекстах, если соблюдаются их контракты. и т.п.

Всё это фактически украдено, причём в весьма лайтовой версии, у программной инженерии, cтабильно рекомендующей это всё последние лет 50 с гаком.
В формализации PFR например леммы были организованы как модули с интерфейсами в Lean.

Математики, что с лицом? :)

=

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

Ну и зачем нам изоморфизм к этой никакой не математике, а по сути, чистой инженерии с эвристиками?

В айтишке это всё работает давно и на порядок качественнее и продуктивнее.

(потерпите, немного додумать осталось :)