Це переклад вступної статті від Филип Уайшчак (Filip Łajszczak) - https://filip.lajszczak.dev/lean-4-with-a-math-textbook—part-0—introduction.html про формалізацію класичної теорії множин від Хелени Расьової у Lean4

У нещодавній розмові Лекса Фрідмана із Терренсом Тао важлива частина розмови була присвячена його відкриттю та використанню Lean 4 для формалізації математики. Тао також говорив про те, наскільки зрозумілою та доступною є мова Lean, і як професійні математики, студенти та аматори можуть її використовувати. Він згадав про проєкт mathlib, що є ініціативою спільноти зі створення єдиної бібліотеки з математики, Equational Theories Project, який він започаткував, а також формалізацію власного підручника з аналізу.

Щоб зробити перші кроки в Lean та доведенні теорем, я хотів почати з чогось конкретного і структурованого. Я знайшов ідеального кандидата в вигляді книги Хелени Расьової «Introduction to Modern Mathematics» - класичному підручнику, що систематично вибудовує математичні основи. Книга Расьової вперше вийшла польською мовою під назвою «Wstęp do matematyki współczesnej» у 1967 році, а англійський переклад був опублікований у 1973-му. Вона мала чотирнадцять майже незмінних видань (останнє у 2004 році) і досі використовується як один із стандартних підручників на курсі «Вступ до математики» у Варшавському університеті, де студентів першого курсу знайомлять з академічною математикою.

Я починаю з самого початку книги - Розділ I, Параграф 1: Поняття множини. Це дуже короткий розділ, всього на 4 сторінки, де розглядаються належність елементів, підмножини та порожня множина. Хоча розділ невеликий, мені знадобилося чимало часу, щоб перекласти його на Lean. Мета перекладу полягає в тому, щоб пояснити матеріал у доступній формі для тих, хто знаходиться на початковому етапі, як колись і я: передбачається знання базових математичних понять, але без попереднього досвіду у формалізації чи комп’ютерно підтримуваному доведенні теорем, проте із певним досвідом у програмуванні. Ретельно прокоментований код доступний у репозиторії. Усі цитати з книги взято з англомовного видання 1973 року.

Але робота над цією формалізацією виявила дещо несподіване: Lean не ґрунтується на тих самих теоретико-множинних засадах, які викладає Расьова. Натомість він використовує так звану теорію залежних типів як свою математичну основу.

Книга Расьової ґрунтується на теорії множин - ідеї про те, що математичні об’єкти є множинами, а математичні твердження описують належність, підмножини та операції над множинами. Натомість теорія залежних типів пропонує альтернативний фундамент: замість множин за базові будівельні блоки беруться типи (наприклад, «натуральні числа» чи «дійсні числа») та функції між ними. «Залежними» типи робить те, що вони можуть залежати від значень - наприклад, тип «вектори довжини n» залежить від конкретного числа n. Це створює багату систему, у якій самі математичні твердження є типами, а докази - це програми, що конструюють значення цих типів.

Хоча це може звучати абстрактно, теорія залежних типів добре підходить для формалізації математики й саме вона лежить в основі сучасних асистентів доведення теорем, таких як Lean.

Коли Расьова публікувала свою книгу наприкінці 60-х, теорії залежних типів у сучасному розумінні ще не існувало. Її концепти лише починали з’являтися завдяки роботам Пера Мартіна-Льофа та інших, розвиваючись паралельно з мовами функціонального програмування у 1970–1980-х роках. Це створює цікаву ситуацію: теорія залежних типів виглядає як просунута, надзвичайно технічна тема, якщо знайомитися з нею через сучасні асистенти доведення, проте вона виступає альтернативною фундаментальною системою для математики - потенційно такою ж базовою, як і теорія множин, яку викладає Расьова.

Формалізація - це не переклад між різними математичними системами, а радше усвідомлення того, що класична математика та типо-теоретичні засади описують одні й ті самі математичні структури, але крізь різні призми. Lean може працювати й з класичною логікою, коли це потрібно, включно з принципами на кшталт закону виключеного третього, які з’являються у другій частині цієї серії.

Тут ми починаємо занурення в «кролячу нору» формалізації тих понять, які математики безтурботно відмахують як «тривіальні» чи «очевидні».

Серія на цей момент: