🔬 Теренс Тао: ИИ обнуляет стоимость генерации идей, превращая верификацию в главное «бутылочное горлышко»
Стоимость генерации гипотез стремится к нулю, но теперь мы тонем в океане непроверенных теорий. Легендарный математик Теренс Тао сравнивает влияние ИИ на науку с появлением автомобилей: технология есть, но старые «дороги» не справляются с трафиком.
Главная проблема сегодня — верификация. ИИ может выдать тысячи вариантов решения задачи, но проверка каждого из них вручную занимает столько же времени, сколько и раньше. По мнению Тао, это полностью меняет роль ученого и инженера: теперь критически важным навыком становится не поиск идеи, а проектирование ворклоу для её автоматической проверки.
Решение Тао видит в инструментах формальной верификации вроде Lean (язык программирования и интерактивное доказательство теорем). Это позволяет проверять выкладки ИИ построчно, исключая галлюцинации и «человеческий фактор».
Вместо решения рутинных задач фокус смещается на выбор правильной проблемы и контроль качества результата. Мы переходим от эпохи дефицита идей к эпохе дефицита доверия к ним, где выигрывает тот, кто быстрее и дешевле умеет отделять рабочие гипотезы от мусора.
#AI #Research #Mathematics #Lean #TerenceTao #FormalVerification
