А вы уже пользуетесь кодексом жпт5.3? :)

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

=>

God-file: слишком много ответственности
В одном файле: определение E8, эквивалентные характеризации, матричный базис, целочисленность, норма, топология, упаковка, плотность.

Сигналы technical debt прямо в коде

Слишком длинные леммы с proof script soup: вынести общий шаг в локальную лемму по индексу/шаблону вектора, убрать copy-paste.

Хрупкие доказательства через simp only/linear_combination..
Такое часто ломается от малых изменений в импортах/леммах simp.
Более устойчиво: маленькие промежуточные леммы с осмысленными именами + меньше глобального simp.

Неочевидные имена h1, h2, hv, this, test и т.д.
Для математики терпимо, но в большом formalization это сильно бьет по читабельности.

Смешение уровней абстракции: рядом стоят высокоуровневые теоремы и низкоуровневые algebraic-manipulation детали.

Чрезмерная зависимость от decide +kernel: для матриц над Q это практично, но читаемость/объяснимость падает.

etc

Математики такие математики. Не имеют ни малейшего представления о базе программной инженерии, которой сегодня владеет любой джуниор. Код ревью? нет, не слышали.