Последние времена наступают: формализовали в Lean результаты филдсовской медали Вязовской про упаковку сфер, AI им конечно помогал. Может, наступила инженерная эра математики? Раньше каждый математик это по сути такой Леонардо да Винчи, сидит, сам мастерит крылья и минисамолёты, чтобы взлетать, ну может с друганами за гаражами. А с Lean это как будто неизбежно 1000 человек будут строить звездолёты, чтобы в космос летать, каждый отвечает за свою деталь, конвейр, контроль качества, и тд (так сейчас устроены массовые проекты у Тао и Конторовича, например). Зачем строить звездолёты (в космос математики) непонятно, правда, но явно дешевле, чем звездолёты в настоящий космос.