Ферма утверждал, что у него есть доказательство его Великой теоремы, слишком большое для поля его записной книжки. Недавно формализация Великой теоремы Ферма в коде Lean привела к ошибке. Эта ошибка была обнаружена во время экспериментов с ИИ для проверки кода. Проблема влияет на то, как функция нарезки строк в Lean обрабатывает чрезвычайно большие позиции. Логически она должна возвращать пустую строку, но скомпилированный код возвращает исходную строку. Это расхождение создает противоречие. Доказатель теорем ошибочно заключает, что пустая строка равна непустой строке. Это позволяет доказать любое утверждение, включая Великую теорему Ферма. Команда Lean исправила ошибку удивительно быстро после ее сообщения. Исправление включало устранение проблем с безопасностью памяти и семантическими несоответствиями. Хотя машинные доказательства вызывают большое доверие, уязвимости могут возникнуть из-за проблем с доказателем теорем. Поэтому тщательная проверка доказательств Lean имеет важное значение.