#theorem proving

И исследования ·17 авг 2026

ИИ Axiom Math формализовал в Lean доказательство теоремы о простых числах с разрывом до 246

Система AxiomProver от Axiom Math создала машинно-проверенное доказательство в языке формальной математики Lean 4 для теоремы о том, что бесконечно много пар простых чисел отличаются не более чем на 246 единиц — это сильнейший известный результат о промежутках между простыми числами. Работа опубликована 17 августа 2026 года как интерактивный blueprint с участием 41 соавтора.

0 47

И исследования ·28 июл 2026

Первая формально верифицированная 3D CSG: как доверять AI-коду без проверки 1000 строк

Разработчик создал первую формально верифицированную реализацию 3D CSG (пересечение мешей) на Lean 4. Вместо проверки 1000+ строк AI-кода достаточно прочитать 93 строки спецификации — корректность гарантирует компилятор Lean. AI автономно написал 60,000+ строк доказательств, которые не нужно читать человеку. Проект работает в браузере через WebAssembly.

0 104

И исследования ·28 июл 2026

Математика доверия к AI: можно ли формализовать истинность, обоснованность и надёжность утверждений модели

Исследователь хочет создать верификационный движок для проверки надёжности утверждений AI — не улучшать LLM, а математически доказывать, можно ли доверять её выводам. Вопрос: как формализовать «истину», «обоснованность» и «доверие» через теорию вероятностей, формальную логику, теорию информации или constraint satisfaction? Ищет математические основы для Trust Engine, а не философские рассуждения.

0 81