Число ван дер Вардена W(2;3,21) = 416: доказано с проверкой ядра Lean 4
Число ван дер Вардена W(2;3,21) = 416: доказано с проверкой ядра Lean 4 Математики получили новое доказательство для числа ван дер Вардена W(2;3,21), которое было предсказано Оливером Куллманном ещё в 2010 году. Теперь установлено, что это значение равно 416. Доказательство выполнено с использованием формальной верификации: каждый шаг проверен ядром системы Lean 4, что исключает ошибки в логических выводах. Числа ван дер Вардена — это классический объект комбинаторики. Они задают минимальный размер множества, в котором при любой раскраске элементов в заданное число цветов обязательно найдётся одноцветная арифметическая прогрессия заданной длины. Для параметров W(2;3,21) речь идёт о двух цветах, прогрессии длины 3 и 21. Ранее было известно, что значение лежит в диапазоне от 389 до 416, теперь нижняя граница подтверждена точным значением. Особенность новой работы — применение интерактивного доказательства в системе Lean 4. Это не просто компьютерный перебор, а формализованное рассуждение, которое можно проверить автоматически. Ядро Lean гарантирует корректность каждого шага, что делает результат особенно надёжным. Для сравнения: многие предыдущие доказательства в этой области полагались на эвристики и частичную проверку. Интересно, что доказательство опирается на методы, разработанные для решения подобных задач в рамках проекта по формализации математики. Это ещё один шаг к тому, чтобы сложные комбинаторные утверждения становились доступными для машинной верификации. Для исследователей, работающих с числами ван дер Вардена, результат важен как подтверждение гипотезы, так и как пример эффективного использования формальных методов. Главное: • Значение W(2;3,21) = 416 доказано формально. • Доказательство проверено ядром Lean 4. • Гипотеза Куллманна 2010 года подтверждена. • Метод применим к другим задачам комбинаторики. #Математика #ФормальнаяВерификация #Lean4 #Комбинаторика #ИИ