2024 року Міжнародна математична олімпіада відзначила історичну віху. Хоча традиційно це змагання є битвою розумів між найяскравішими студентами світу, неофіційний учасник вкрав усю увагу: AlphaProof від Google DeepMind. Програма на базі ІІ показала результат рівня срібної медалі, довівши, що машини більше не просто обчислюють числа – вони починають освоювати мистецтво логічного міркування.
Цей прорив не є ізольованим дивом інженерної думки; це результат десятирічної еволюції того, як ми перевіряємо істину за допомогою коду. У своїй новій книзі «Доказ у коді» (The Proof in the Code) журналіст Кевін Хартнетт досліджує неймовірний шлях Lean — програмного інструменту, який перетворився з нішевого помічника для кодингу на фундамент сучасної математичної верифікації та розробки ІІ.
Міст між кодом та логікою
Історія починається з Лео де Моури, колишнього інженера Microsoft Research, який запустив Lean у 2013 році. Спочатку розроблений як інструмент для перевірки програмного коду на наявність помилок, Lean мав прихований потенціал завдяки своїй структурній схожості з математикою.
Як зазначає Хартнетт, ці дві дисципліни мають загальну фундаментальну ДНК:
– Синтаксис: Обидві вимагають точних, покрокових інструкцій.
– Логіка: Єдина помилка в рядку коду функціонально ідентична пробілу в математичному доказі.
– Виконання: Подібно до того, як програма запускається тільки за наявності вірної логіки, математична теорема вважається вірною лише тоді, коли її доказ бездоганний.
Це розуміння дало поштовх новому руху. Хоча Lean не міг самостійно «винаходити» нову математику, він виступав у ролі інтерактивного доказника теорем. Він міг взяти написаний людиною доказ — який міг займати сотні сторінок та місяці рецензування — і миттєво підтвердити його абсолютну коректність.
Боротьба за «математичну мову»
Перехід від традиційної математики до цифрових доказів був гладким. Роками математики стикалися з класичною проблемою «курки та яйця»: щоб зробити Lean корисним, їм потрібні були величезні бібліотеки закодованих математичних визначень; але щоб створити ці бібліотеки, їм потрібні були математики, які використовують програму.
Тертя часто були абсурдно деталізованими. Хартнетт описує, як професор Кевін Баззард з Імперського коледжу Лондона, викладаючи студентам, зайшов у глухий кут, тому що Lean вимагав від нього довести, що 2 не дорівнює 1. Для людини це очевидна істина; Для системи формальної логіки це фундаментальний факт, який має бути явно визначений, перш ніж можна буде приступати до будь-яких подальших міркувань.
Подолання цих перешкод зажадало колосальних колективних зусиль:
* Масштабна цифровізація: У 2018 році математики витратили місяці, переводячи складні концепції, такі як «перфектоїдні простори», у тисячі рядків коду.
* Створення спільноти: Невелика група відданих справі дослідників працювала над тим, щоб зробити програмне забезпечення зручним, перетворивши його з громіздкого академічного інструменту на надійну платформу.
* Масштабування: До 2025 року екосистема зробила вибухове зростання: десятки тисяч користувачів з академічного середовища та технологічної індустрії зробили свій внесок у бібліотеки Lean.
Чому це важливо: Пошук «машини істини»
Злиття математики та ІІ – це кінцева мета даного руху. Для інженерів-програмістів, таких як де Моура, призом була «машина істини», здатна гарантувати, що таке програмне забезпечення, як Microsoft Word, буде повністю позбавлене багів. Для математиків це спосіб гарантувати, що навіть найскладніші та абстрактні відкриття не будуть піддані сумніву.
Для дослідників ІІ Lean є ідеальним полігоном для навчання. Надаючи величезну верифіковану бібліотеку математичних істин, Lean дозволяє таким моделям, як AlphaProof, освоювати суворі міркування, а не просто розпізнавання патернів. Це критично важливо для вирішення проблеми галюцинацій ІІ — схильності моделей впевнено заявляти хибну інформацію. Якщо ІІ можна навчити дотримуватися суворих, непохитних законів математичної логіки, згодом він зможе застосувати цю ж строгість до міркувань у реальному світі.
«І [математика, і програмування] записуються з точним синтаксисом як серія логічних кроків, кожен із яких веде до наступного».
Висновок
Книга «Доказ у коді» розповідає про те, як спеціалізований інструмент для налагодження програмного забезпечення став основою для нової ери математичної достовірності та інтелекту ІІ. Вона підкреслює глибоке зрушення в науці: рух до майбутнього, де людська інтуїція та цифрова верифікація працюють у тандемі, щоб визначати, що є істиною.
