AxiomProver впервые формально проверил теорему 246 о простых числах
AxiomProver впервые формально проверил теорему 246 о простых числах Компания Axiom Math с помощью своей ИИ-системы AxiomProver впервые получила полностью машиночитаемое доказательство теоремы 246: бесконечно много пар простых чисел отличаются не больше чем на 246. Это лучший известный результат на пути к гипотезе о простых-близнецах. Теорему в 2010-х довели до такого вида коллаборация Polymath8b с участием Джеймса Мейнарда и Теренса Тао. Теперь весь ключевой фрагмент формализован в Lean 4 и собран в открытую библиотеку PrimeGapsLib. AxiomProver — автономная мультиагентная система, которая сама переводит математические утверждения в проверяемые доказательства. По словам основателя Кен Оно, этот результат — «порог человеческих знаний о простых числах». Такой подход уже смотрит дальше математики: формальная проверка может стать инструментом доверия к коду, который пишет сам ИИ. Источники: https://spectrum.ieee.org/axiom-math-246-theorem-formalization https://primegaps.axiommath.ai/ https://github.com/AxiomMath/PrimeGapsLib #AI #AxiomMath #Lean #PrimeGaps #MathAI #FormalVerification