Фонд Simons выделил 15 млн долларов на проверку машинных доказательств

Simons Foundation открыл программу на 15 млн долларов, чтобы математики разобрались в доказательствах, полученных с помощью моделей. Пять миллионов вносит OpenAI, часть — Anthropic; обе лаборатории дополнительно выделяют исследовательский доступ.

Деньги идут на разбор свежих машинных результатов, освоение инструментов и выработку общих правил того, как ссылаться на такие доказательства и как их проверять. Фонд раньше финансировал систему формальных доказательств Lean.

Контекст у инициативы невесёлый: часть математиков уже отказывалась бесплатно вычитывать работы моделей, а в проверенных доказательствах OpenAI находили расхождение между формальной записью и словесной формулировкой.