Яндекс.Метрика
AI-дайджест·Пачка
← Дайджест от 11 октября 2026
Исследования3 источникаHN 323TG 14k

Математик Теренс Тао прочитал лекцию «Math 2.0» о работе в эпоху машинных доказательств

Теренс Тао — один из самых известных действующих математиков — прочитал в Калтехе лекцию «Math 2.0» о работе в условиях, когда доказательства помогает искать машина, и выложил слайды. Изначально он собирался читать её под названием «Доказательство с помощью машины», но, по собственному признанию, содержание заметно изменилось из-за недавних событий.

Главный тезис: математика веками исходила из того, что открытая задача решается редко и трудно. Вокруг этого выросли институты, карьерные стимулы и способ публиковать результаты. Если решения перестают быть редкими, перестраивать придётся и методы, и само устройство профессии.

Слайды собрали 375 комментариев на Hacker News — спор идёт о том, что считать авторством доказательства, когда ключевой шаг нашла модель.

Что говорят
qupHacker News
«Захотите ли вы перед уколом знать, что хотя бы один человек понимает механизм этого лекарства?» Нет. Я же умираю, дружище. У этого человека, может, самый высокий IQ на планете, но видно, что он мало общался с обычными людьми: почти никто и сейчас толком не понимает, что глотает, кроме эффекта. Да, я приму лекарство от рака, которого не понимает ни один человек, и миллиарды примут — лишь бы лечило.
squidmasterHacker News
Тао лезет не в свою область: у кучи лекарств механизм не изучен. Мы до сих пор не разобрались, как именно работает общий наркоз, — откажетесь от него, когда вас будут вскрывать, чтобы удалить опухоль?
19298857Hacker News
Насчёт «математики 2.0» я не уверен: ИИ может отлично находить бесполезное — вроде «P==NP, но сложность O(n^4242424242424242)». К тому же люди становятся формалистами и теряют привычные источники вдохновения; возиться с Lean, наверное, стоит специалистам, а не творческим математикам у доски.