Hacker News Digest

11 октября 2026 г. в 13:16 • teorth.github.io • ⭐ 294 • 💬 352

Original • HN

#ablation-studies#ieantn#lean#llm#math#mathathon#theorem-proving

Terence Tao: Math 2.0 [pdf]

Математика переживает переход от эпохи дефицита доказательств к эпохе их изобилия благодаря развитию ИИ. Традиционно поиск и проверка доказательств требовали глубокой экспертизы и были редки, что формировало институты и стимулы математической науки. Однако доказательства обладают уникальными свойствами: они объективно проверяемы, легко оцифровываются и могут быть верифицированы машинами, например, в системах типа Lean. Это делает математику идеальной мишенью для современных ИИ-моделей, которые уже способны решать многие открытые задачи за короткое время без специального prompting от пользователя. Однако способности ИИ крайне неровны: впечатляющи в формальных, данных-rich задачах, но слабы там, где требуется субъективная оценка или взаимодействие с реальным миром.

Несмотря на прогресс, большинство проблем на переднем крае математики остаются нерешёнными — пространство задач бесконечно, а их сложность неограниченна. Поэтому будущее математики — «Math 2.0» — должно выходить за рамки простого поиска доказательств. Нужно смещать фокус с количества на качество: использовать ИИ для выявления новых принципов, методов и инсайтов, улучшать существующие доказательства, исследовать «окрестности теорем», строить интерпретируемые и безопасные открытые математические модели. Примеры включают Maththon — студенческий марафон по улучшению доказательств, IEANTN — динамическую сеть результатов в аналитической теории чисел, и ablation studies — проверку устойчивости théorems при удалении посылок. Главное препятствие для Math 2.0 — не технологии или культура, а воображение: умение видеть, как ИИ может углубить понимание, а не просто автоматизировать поиск.