Post #70

Google запустили коллекцию нерешённых математических задач,записанных на языке Lean Это подготовка инфраструктуры для качественно нового этапа развития ML Сейчас математические бенчмарки для LLM тестируют школьную и студенческую математику GSM8K, MATH — задачи с известными решениями Formal-conjectures — это нерешённые проблемы Разница как между контрольной работой и диссертацией У DeepMind есть AlphaProof для автоматического доказательства теорем Есть Lean для формальной верификации Теперь появляется стандартизированный набор открытых проблем Экосистема собрана Когда ML решит первую серьёзную математическую гипотезу, это станет переломным моментом Но без готовой инфраструктуры для верификации и сравнения систем этот момент может быть упущен или оспорен DeepMind создаёт "математический ImageNet" — эталон для научного применения ML Кто контролирует стандарты, тот получает преимущество в гонке Контролируя стандарты и инфраструктуру для оценки математического ML, Google получает преимущество перед конкурентами (OpenAI, Anthropic и др.) Это инвестиция в будущее, где математический ML станет ключевой технологией