Lean стикається з питаннями надійності доведення теорем у міру розвитку автоформалізації з AI

Формалізація та автоформалізація

Lean став найпопулярнішим серед математиків інструментом для доведення теорем, згідно з гостьовим дописом математика Томаса Хейлса. Його створив Лео де Моура у 2013 році, працюючи в Microsoft; Microsoft згодом опублікувала програму з відкритим кодом. Lean базується на теорії типів, зокрема на діалекті числення індуктивних конструкцій. Його громадська бібліотека mathlib, яку було розпочато у 2017 році, тепер охоплює близько 300 000 теорем, понад 100 000 визначень, 2,5 мільйона рядків коду та понад 700 контриб'юторів. Будь-яку теорему mathlib можна використовувати в наступних доведеннях замість нового доведення.

Автоформалізація, коли AI читає роботу та видає формальне доведення, стала практичною реальністю у 2026 році. Серед важливих етапів: квазі-автоформалізація простої теореми про числа компанією Math Inc. у вересні 2025 року; формалізація великої частини підручника з топології Munkres; задача про упаковку сфер у 24 вимірах; автоформалізація останньої теореми Ферма компанією Anthropic 4 вересня, яка згенерувала 13 мільйонів рядків Lean за 11 днів; та формалізація спалахів Navier-Stokes від OpenAI, оголошена 8 вересня.

Дизайн і модель надійності

Lean поєднує універсальну мову програмування з математичною мовою для визначень, формулювань теорем і скриптів доведення. Скрипти доведення розбирає, обробляє та перевіряє ядро Lean — кілька тисяч рядків C++-коду. У дописі наголошено, що доведення Lean необхідно завжди перевіряти ядром і що потрібен окремий людський аудит для підтвердження відповідності формулювання, щоб переконатися, що доведена теорема справді є тією теоремою, яку мають на увазі математики.

Лето вад надійності

Проблема надійності — це проблема ядра, яке приймає доведення „False“ і, отже, доводить будь-яке твердження. Кілька таких вад у Lean виявили у липні та серпні 2026 року, що тепер називають летом вад надійності. Одна вадa спричинила некоректне спростування гіпотези Колатца, інша — некоректне коротке доведення гіпотези Кеплера. Усі їх швидко виправили, а mathlib перевірили виправленим ядром.

Пропозиції та відкриті проблеми

Розглядаються три підходи. Перший: написати додаткові ядра Lean і перехресно перевірити доведення; існує близько 25 ядер, а формальнізацію Navier-Stokes підтвердили понад десять перевірників доведень. Другий: формально перевірити ядро, як це зробив Йоахім Брайтнер за допомогою Con-Leche, підтвердивши узгодженість ядра Lean, доведення якого згенеровано Claude і яке перевірило mathlib. Третій: поглибити теоретичне розуміння теорії типів Lean, де залишаються відкритими унікальна типізація, ін'єктивність Pi, змінена властивість Church-Rosser та повна публічна відносна узгодженість. Публікація завершується цитуванням „Reflections on Trusting Trust“ Кена Томпсона і попередженням, що сліпо довіряти системам типу Lean більше не можна.

Джерела: terrytao.wordpress.com