У нас есть 3 «теории всего» — научная картина мира (все сводится к законам физики), информатика (все сводится к битам) и фундамент математики (все сводится к логике). Именно фундамент математики представляет особый интерес, так как он является фундаментом для двух других фундаментов и имеет глубокий философский смысл. Последние 2 года (2023–2024) я сильно им увлекся и проделал довольно большую работу по углубленному изучению теории типов (Calculus of Constructions), и готов поделиться результатами, а также рассказать о девяти направлениях, где можно применить это на практике. Очень многое получилось лучше, чем я планировал. Изначально перспективы были не очень понятными, и поэтому я не рассказывал друзьям и коллегам про мою работу в этом направлении и называл это «Секретный Проект». Но теперь, когда многое прояснилось и получилось, можно поделиться успехом. Собственно, в этой статье я расскажу вам не только про сам фундамент математики, а еще его связь с ежедневной работой программиста, а также с Computer Science/Data Science и AI/ML. Я вам нарисую большую и красивую картину, на которой все понятно и логически следует из маленького набора правил выведений типов (11 штук) и аксиом теории множеств (9 штук).
У нас есть 3 фундамента математики — теория множеств (удобна для человека), теория типов (удобна для компьютера) и теория категорий (не знаю, зачем она вообще нужна). Они примерно одинаковой мощности и одну можно выразить внутри другой. Особый интерес представляет именно теория типов, т.к. ее довольно легко можно запрограммировать внутри компьютера и использовать как строгий фундамент для других теорий, который не дает совершить ошибку и проверяет каждое ваше действие.
А сейчас я вам расскажу короткую историю теорем‑пруверов (пруф‑ассистентов) — это такие программы, которые позволяют доказывать математические теоремы и строить на их основе фундамент математики с нуля. В 1973 появился проект Mizar (в Польше) и он был первым успешным теорем‑прувером. На данный момент его библиотека — самая большая (52,000 доказанных теорем и 10,000 математических определений).
Разработчики Mizar попробовали создать теорем‑прувер полностью на теории множеств (что казалось логичным на тот момент), но в итоге получился огромный архитектурный костыль — им пришлось поддерживать 2 ядра одновременно (теория типов и теория множеств) вместо одного. Это плохо не только для разработки/поддержки системы, но и для освоения\обучения\расширения.
Прошло время и теория типов сформировалась как отдельная дисциплина, хорошо проработанная и сформированная. Исследователям удалось очень чисто (без костылей) выразить математическую логику внутри теории типов, и сделать ее 100% совместимой с тем, как думают математики. Как им удалось до этого догадаться и сделать такой большой прорыв — я не знаю. Так вот, если мы полностью формализуем математическую логику, то аксиоматическая теория множеств очень чисто и легко выводится из нее. Нужно всего лишь аксиоматически задать существование отношения принадлежности к множеству (∈), а также добавить 9 аксиом ZFC (Zermelo‑Fraenkel Set Theory), которые по сути постулируют существование двух множеств (пустое и бесконечное) и как с ними работать. А саму формальную систему математической логики (набор правил) называют Натуральная Дедукция.
Есть 2 популярные теории типов — Martin‑Löf type theory (MLTT) и Calculus of Construction (CoC). Они примерно одинаковой мощности и имеют скорее культурную\территориальную разницу. Тем не менее, Calculus of Construction немного новее и компактнее, а также используется двумя самыми популярными в индустрии теорем‑пруверами — Coq и Lean. А еще по ней есть супер‑качественный и новый учебник от Роба Недерпелта (Type Theory and Formal Proof: An Introduction). Поэтому я выбрал именно ее.
Собственно, 80% моих усилий по изучению фундамента математики на протяжении последних двух лет построены вокруг этой офигенной книги. Авторы книги проделали огромную работу и проанализировали 147 источников (другие книги и статьи), чтобы собрать все самое лучшее в одном месте. Благодаря их труду, я освоил эту область всего за 2 года вместо 10 лет. Я прорешал почти всю книгу и почти все упражнения, полностью покрыв первые 13 глав (300 страниц) книги. Эта книга строит фундамент математики с полного нуля и объясняет\формально вводит вообще все концепции и нотации. Одна из интересных особенностей книги в том, что автор использует современный конструктивный подход и выражает математическую логику полностью конструктивным способом, не использовав таблицу истинности ни разу. Это очень хорошо для обучения и понимания, а также наглядно показывает, как теория типов может переплетаться с математической логикой и чем на самом деле являются многие логические операции на низком уровне.
Можно разбить содержимое книги на 3 части — в первой части (1 — 6 главы) автор с полного нуля (с лямбда‑исчисления) постепенно достраивает и усложняет систему типов и проходится по всему лямбда‑кубу, чтобы получить в итоге золотую классику — Calculus of Constructions (λC). Во второй части (7 — 13 главы) — автор рассказывает, как запихнуть в эту теорию типов математическую логику и теорию множеств. В третьей части (14 — 15 главы) автор формализует целые числа (Z) и их арифметику внутри теории типов, дает основы теории чисел, а также формализует доказательство теоремы Безу в качестве демонстрации работы системы типов.
Собственно, главы 1–7 я прорешал на бумаге (со 100%‑м покрытием всех упражнений в конце глав), потом я написал маленькое мобильное приложение под андроид (MathConstructor) и в нем покрыл главы 5,6,7 и 11. Главы 11–13 я покрыл уже внутри Coq, исходники можете найти в моем GitHub. И это получилось очень круто и полезно и эффективно! А на 14–15 главы у меня не хватило мотивации, т.к. в 13-й главе автор не очень чисто покрыл теорию множеств. Он решил использовать гибридный подход (с костылями внедрить многие концепции теории множеств в теорию типов, вместо того, чтобы чисто выводить все из аксиом ZFC). Мне это совсем не понравилось и пришлось переключиться на другой учебник по теории множеств.
Главы книги, их покрытие, оценка сложности и инструменты, которые я использовал для обучения
№ | Глава | Сложность | Мое покрытие | Я использовал | Рекомендую вам |
1 | Untyped lambda calculus | 9 | 100% | Pen & Paper, Anki | Pen & Paper, Anki |
2 | Simply typed lambda calculus | 6 | 100% | Pen & Paper, Anki | Coq |
3 | Second order typed lambda calculus | 5 | 100% | Pen & Paper, Anki | Coq |
4 | Types dependent on types | 5 | 100% | Pen & Paper, Anki, Custom App | Coq |
5 | Types dependent on terms | 5 | 100% | Pen & Paper, Anki, Custom App | Coq |
6 | The Calculus of Constructions | 5 | 100% | Pen & Paper, Anki, Custom App | Coq |
7 | The encoding of logical notions in λC | 7 | 100% | Custom App | Coq |
8 | Definitions | 4 | 100% | Pen & Paper | Coq |
9 | Extension of λC with definitions | 5 | 100% | Pen & Paper | Coq |
10 | Rules and properties of λD | 5 | 100% | Pen & Paper | Coq |
11 | Flag‑style natural deduction in λD | 7 | 100% | Custom App, Coq | Coq |
12 | Mathematics in λD: a first attempt | 6 | 100% | Coq | Coq |
13 | Sets and subsets | 7 | 100% | Coq | - |
14 | Numbers and arithmetic in λD | 8 | 0% | - | - |
15 | An elaborated example | 7 | 0% | - | - |
16 | Further perspectives | 3 | 100% | - | - |
Собтсвенно, после 13й главы я рекомендую вам переключиться на книгу по теории множеств
Собственно, я взял старый и классический учебник по теории множеств от 1963 года (Set theory and logic by Robert Stoll), и сразу прыгнул на 7 главу (Informal Axiomatic Set Theory), которая дает аксиомы ZFC и выводит из них множество натуральных чисел и его базовые свойства, и формализовал примерно половину главы за месяц. Это была проверка теории типов и Coq на прочность — и проверка успешно пройдена! Я был поражен тем, насколько автор 1963 года все четко излагает. Даже самые странные его утверждения и математические конструкции оказались очень нужны и полезны при формализации. Все его шаги, 100% ход мыслей можно 1–1 перенести на формальный язык теории типов. В общем, мне опять повезло с книгой, хоть там и много технических опечаток, но они — не проблема. Я точно уверен, что вернусь к этой книге еще.
В итоге, мне всего за месяц удалось закрыть огромное количество «серых зон» и пробелов в понимании ключевых математических концепций, которые у меня образовались в 2021 — 2022 году по мере прохождения различных стандартных математических курсов типа Calculus I / II / III. Мне удалось доказать существование множества натуральных чисел (N) — вытащить его из аксиомы бесконечности (ZF_Infinity), а также вывести 5 аксиом Пиано (на них все числовые системы строятся), а еще вывести принцип математической индукции, а из него — вывести принцип сильной индукции. Еще мне удалось из общей аксиомы выбора (ZF7_Choice) вывести частную аксиому выбора (более удобную), а из нее (используя теорему Диаконеску) вывести аксиому исключения среднего (excluding third), на которой базируется вся неконструктивная (классическая) математика. И все это очень интересно и полезно. Многие аксиомы для меня больше не являются аксиомами, а выводятся из 9 аксиом ZFC. Мне очень нравиться такой подход. Возможно, мне близка философия логистов и формалистов.
В итоге, на основе этих двух книг по теории типов и теории множеств, мне удалось заложить основы собственной библиотеки Coq, которая написана полностью с нуля и которую я понимаю на 100% как она работает изнутри. Я долго думал, как ее назвать, и ChatGPT предложил мне название ZFCFramework. Так и назовем ее. Собственно, в ближайшие пару лет я планирую ее активно развивать и наращивать, применять для разных обучающих целей. Очень круто, что у меня теперь есть такой инструмент. Если я буду погружаться в разные разделы математики и проходить новые курсы, я могу параллельно формализовать их в Coq и усиливать фундамент, а также получать максимальный выхлоп и максимально глубокий результат от потраченных сил на курсы или учебники.
По поводу моего мобильного Android‑приложения MathConstructor: я пока его нигде не выкладывал, но планирую выложить где‑нибудь в 2025 году вместе со всеми исходниками, и под это будет отдельная статья. Но вам не обязательно ждать — вы можете разработать свой аналог — и это совсем не трудно! На разработку рабочей Calculus of Constructions мне понадобилось всего 4 дня, и главы 5–6–7 уже почти полностью покрывались. Еще две недели понадобилось на баг‑фикс, всякие удобства и допиливания λC до λD. Как говорил Кнут, «Лучший способ в чём‑то разобраться до конца — это попробовать научить этому компьютер». Именно разработка приложения с нуля даст вам 100%‑е понимание материала, а если вы будете использовать мое приложение — то только 90–95%. Возьмите шрифт Euler и любой HTML‑движок, и этого достаточно для представления любого материала из книги.
Если вы достаточно умный и смелый — можете сразу же прыгнуть на главу 11 в книге по теории типов и программировать математическую логику/решать логические задачи внутри Coq, и возвращаться на предыдущие главы по мере возникновения вопросов. И использовать мои исходники, в которых я на 100% формализовал все содержимое главы и все упражнения в конце главы, для справки и при возникновении трудностей. У меня получилось 700 строк кода, это не очень много. Тут надо еще заметить, что я полностью отключил стандартную библиотеку Coq (опция '‑noinit'), а также не использовал индуктивные типы, которые очень популярны в сообществе Coq‑loving mathematicians.
По поводу первой главы — она довольно емкая и дает основы лямбда‑исчисления. Весьма желательно прорешать ее на бумаге, если вы не имели опыта с теорией лямбда‑исчисления. Coq не совместим с Untyped lambda calculus, так что его не получится использовать для самопроверки. Если вы знаете среду (или язык программирования), которые совместимы с не типизированным лямбда исчислением и позволят формализовать содержимое главы в них и проводить вычисления\проверки, то обязательно напишите об этом в комментариях. Если сможете прорешать первую главу в такой среде — обязательно выложите исходники и пришлите мне ссылку. Я бы сам не прочь вернуться на первую главу и повторить материал.
А что касается аксиоматической теории множеств (ZFC), то у нее есть очень много преимуществ и есть сильная мотивация для ее освоения. ZFC появилась 100 лет назад и на протяжении века все разделы математики были корнями под нее подведены. Любой классический учебник математики можно к ней свести 1–1, даже если неявно на нее не ссылаются. Конечно, есть и другие теории множеств. Например, проект Mizar использует теорию множеств Тарского‑Гротендика (TG), и она немного посильнее ZFC. Но у меня пока не попадалось реальных случаев, когда бы не хватало ZFC.
Если вы хотите короткую серию из вводных лекций по ZFC, я могу вам порекомендовать плейлист от Ричарда Борчердса на YouTube. Он — один из самых крутых математиков в мире, получал Филдсовскую премию в 1998 году — одну из самых престижных наград в математике (ее часто называют «Нобелевская премия для математиков»). Ричард записал бесплатную серию из 8 видеоуроков и разборал все аксиомы ZFC, довольно четко и емко. Я полностью посмотрел и законспектировал его в 2023 году за полторы недели.
Математику часто делят на 2 типа — вычислительную (нахождение производных\решение уравнений и так далее), а также на аксиоматическую (proof‑based/rigorous). Именно второй тип является «настоящей» математикой. Можете почитать про математическую зрелось (Mathematical maturity) и теория типов как раз помогает ее гарантированно достичь. Терренс Тао предложил разделить математическое образование на 3 этапа — Pre‑rigorous/Rigorous/Post‑rigorous. Собственно, формализация математики помогает максимально и идеально прокачать второй этап (Rigorous), и именно на нем обычно застревают большинство студентов.
Я довольно хорошо учился в универе на IT‑факультете (Институт вычислительных систем и программирования (Институт 4) в СПБ ГУАП), и даже получал награду «Студент года ГУАП — 2017». В целом, там была хорошая образовательная программа, но некоторые моменты можно точно улучшить на уровне ГОСТ‑стандартов. Один из таких моментов — это слишком много лекций по теоретическим предметам и отсутствие семинаров по ним с акцентом на покрытие (построение) теории. Пример 1 — у нас был предмет «Абстрактная Алгебра», который был мне интересен. Но семинары по ней не соответствовали тому, что давалось на лекциях — на них мы решали вычислительные задачи вместо доказательства теорем с нуля. Пример 2 — у нас был предмет «Математический Анализ», но на семинарах мы тоже решали вычислительные задачи в большом количестве — нахождение производных и интегралов. Мне кажется, это пережиток прошлого и ГОСТ нужно менять. Лекции, как формат обучения, нужно вообще выпилить. Они имеют очень мало смысла в современном мире. Всегда можно найти записи и просмотр лекции вживую — это, по сути, тоже самое, что и просмотр записи онлайн, только неудобен и будет почти всегда ниже по качеству, чем хорошо подготовленная запись. Вместо лекций, нужно делать много‑много семинаров с небольшими группами студентов по 5–8 человек. Профессор на семинаре может давать тот же материал, что и на лекции, но выводить и доказывать его одновременно со студентами, и делать паузы\давать студентам возможность быть частью этого процесса. Это будет дороже для ВУЗа, но разница вряд ли будет ощутима для руководства.
Еще нужно предупредить вас об одном заблуждении, которое весьма распространено как на Хабре, так и (по всей видимости) среди студентов. Существует пресловутая теорема Геделя о неполноте, которая звучит так: в любой достаточно мощной формальной системе существуют истинные утверждения, которые нельзя доказать в рамках этой системы. И я часто встречал некорректную (неправильную) интерпретацию этой теоремы. Некоторым кажется, что из этой теоремы следует невозможность создания единого фундамента, из которого все выводится. Но ведь такой фундамент есть и уже сто лет существует — и это 9 аксиом ZFC! Можете спросить у ChatGPT, «Какие разделы математики невозможно формализовать в ZFC?» — и он вам накинет весьма редкие случаи, половина из которых (внезапно) из разных глубоких разделов теории множеств. Если вы столкнетесь с этими редкими случаями, вы можете просто накинуть дополнительные аксиомы к ZFC. Например, гипотеза континуума (CH) — вполне себе кандидат на добавление в ZFC, но ее не стали добавлять, т.к. она просто никому особо не нужна. Я не проверял, но полагаю, что можно вывести все ключевые теоремы и утверждения о современных нейронных сетях, и гипотеза континуума при этом не будет использована.
До 2023 года, моей главной целю в изучении теории\фундамента математики было разобраться в фундаменте высокоуровневых математических дисциплин — теории вероятности и математической статистике. Под ними лежит довольно длинный математический стек. Начиная с 2023 года, я переключил главную цель на «разобраться в фундаменте AI». Как выяснилось, эти цели почти полностью совпадают. На основе теории типов вы строим математическую логику, далее на основе логики — строим теорию множеств, затем переходим к построению числовых систем и доказываем существование натуральных чисел на основе аксиомы о бесконечности, далее строим целые и рациональные числа на основе натуральных чисел. После этого можно построить множество вещественных чисел на основе рациональных чисел и перейти к анализу вещественных чисел. Далее, переходим к теории измерений и строим теорию вероятности на ее основе. Далее, независимо от всего этого можно вывести линейную алгебру из теории вероятности. Когда у нас есть теория вероятности и линейная алгебра, можно переходить к математической статистике, а после нее — уже строить конкретные модели нейронных сетей.
Чтобы понять, на каком фундаменте построено современное машинное обучение — можно ссылаться на курсы Mathematics for Machine Learning Specialization (Coursera) и Mathematics of Machine Learning (MIT). Видим, что в списке фигурирует Real Analysis/Linear Algebra/Probability/Statistics/Multivariate Calculus/PCA. У меня сложилось впечатление, что самым важным из этого списка является Real Analysis (вещественный анализ, на русском языке часто его называют просто «математический анализ» или матан), а Calculus III (мультивариативное исчисление) и Probability (теория вероятности) из него выводятся. А статистика, точнее самая вкусная ее часть, выводится из теории вероятности.
Таким образом, центральной задачей в освоении фундамента машинного обучения является формализация математического анализа. Эта задача не нова и решилась еще в 1977 году, когда один студент (аспирант) использовал теорем‑прувер Automath, чтобы формализовать учебник «Основы анализа» (Foundations of Analysis) Эдмунда Ландау и защитил диссертацию на эту тему. Как оказалось, математический анализ очень даже хорошо формализуется. Это очень важный предмет, для понимания которого как раз требуется мыслить через строгую математическую логику, и многие вузы используют его для отсеивания студентов, которые не осилили формальные методы мышления и вместо этого мыслят эмоционально и живут животными инстинктами.
Среди западных авторов, есть 3 хороших учебника по математическому анализу. Самый классический — это Principles of Mathematical Analysis by Walter Rudin, он чаще всего используется в англоязычных технических вузах. Он хорош с точки зрения формальной подачи, глубины проработки и сложных упражнений. Главный недостаток для меня в том, что он аксиоматически задает множество вещественных чисел R (11 аксиом поля и аксиома полноты), вместо того, чтобы выводить все из теории множеств. В этом есть свои плюсы, тк строить всю цепочку числовых систем может отнять много сил и времени. Например, в другом учебнике (Analysis I by Terrence Tao), автор тратит первые 100 страниц книги, чтобы построить числовые системы (N → Z → Q → R) на основе аксиом Пиано. Есть еще книга Understanding Analysis by Stephen Abbott, и у нее очень высокая популярность среди современных студентов (судя по отзывам на амазон). Я прорешал первую главу в 2022 году, но мне она не зашла, т.к. она слишком неформальная и слишком много пробелов\дыр в понимании оставляет. Я бы предпочел потратить в 3–5х больше усилий и пройти книгу Рудина или Терренса, но получить хороший результат без пробелов в понимании.
Собственно, книга Set theory and logic by Robert Stoll от 1963 года тоже строит всю цепочку числовых систем (N → Z → Q → R). Но, как мне кажется, Терренс Тао делает это более подробно и потом плавно перетекает в теоремы анализа, ряды и интегралы. Скорее всего, я пойду именно этим путем, т.к. на основе рядов и интегралов можно потом строить теорию вероятности. Например, в книге A First Look at Rigorous Probability Theory by Jeff Rosenthal, есть раздел «A. Mathematical Background», и автор рекомендует использовать его как измерение «входного порога» (пропускной экзамен) в аксиоматическую теорию вероятности. Если вы чувствуете себя комфортно в тех темах, что там указаны — можно переходить к этой книге. Собственно, там половина — теория множеств, а другая половина — это ряды и свойства вещественных чисел.
Входной порог в аксиоматическую теорию вероятности - что требуется знать
Есть 2 способа формализовать множество вещественных чисел ® — через разрез Дедекина (дается в книге Рудина и Столла) и через последовательность Коши (дается в книге Терренса). Я пока не разобрался в этой теме, но, скорее всего, пойду по второму пути (Cauchy sequences), т.к. это более чистый и современный подход, а также последовательности\ряды более релевантны к фундаменту теории вероятности. Но любой способ подойдет, главное, чтобы на итоговом множестве работали (выводились) аксиомы поля, порядка и полноты.
Что касается линейной алгебры — тут можно ссылаться на учебник Linear Algebra Done Right by Sheldon Axler. Если хотите посмотреть конкретную демку, как главы этой книги формализовать внутри Coq, можете посмотреть плейлист Linear Algebra Done Right in Coq, в котором профессор Квин записал 50 часов видеоуроков. Это может повысить вашу мотивацию и дать конкретный пример. Я планирую повторить тоже самое, но мой фундамент математики будет более чистый (без индуктивных типов), а также полностью выводиться из ZFC.
А если вам нужен хороший курс по Calculus III (мультивариативное исчисление), то я могу порекомендовать курс на Educator (23 часа, довольно емкий и приятный). Я его полностью прошел пару лет назад и научился брать тройные интегралы на бумаге параллельно с автором.
Далее, нужно выяснить, на каком математическом фундаменте построен ChaptGPT. Тут можно ссылаться на курс Neural Networks: Zero to Hero, в котором автор строит GPT-2 с нуля. У меня сложилось впечатление, что математический фундамент генеративных нейронных сетей (внезапно) не отличается от обычных нейронных сетей и уходит корнями в классическое машинное обучение. Но я глубоко не копал эту область, и если я не прав, просьба в комментариях подробно раскрыть эту тему.
Тут надо заметить, что конечный результат работы генеративных нейронных сетей на данный момент является чем‑то типа черного ящика и (насколько я понял) не формализуется. Я думаю, это вопрос времени. Программирование тоже когда‑то считалось скорее искусством, чем наукой. А потом пришел Кнут и подвел четкий математический фундамент под анализ сложности и корректности алгоритмов, переиспользовав при этом существующий математический аппарат алгебры\исчисления\теории множеств и теории графов, а также украв нотацию O большого у Ландау. Я уверен, что с нейронными сетями произойдет тоже самое. Я на 80% уверен, что там будут переиспользованны какие‑то существующие разделы математики, которые уже существуют и полностью совместимы с ZFC. Я на 95% уверен, что даже если появятся новые разделы математики, то их сделают совместимыми с ZFC. Я на 99% процентов уверен, что даже если и появится новый фундамент математики, то его можно будет выразить внутри теории типов и формализовать внутри Coq.
Также, есть интересная книжка Neural Networks from Scratch (https://nnfs.io/), в котором авторы используют только питон и его стандартные библиотеки, чтобы построить простые нейронные сети. Я ее пока не пробовал, но планирую в обязательном порядке попробовать в будущем. Для обучения, именно такие подходы максимально хороши.
Если вам интересна тема прохождения онлайн‑курсов в целом, то я на прошлой работе (когда работал в Сравни Java‑разработчиком) записал большой митап на эту тему, можете посмотреть запись вот тут. А сейчас, я работаю в EDNA Java‑разработчиком.
Анонс моего митапа по онлайн-курсам
Это Ярослав, Java‑разработчик из команды Core/AF. Месяц назад я сделал опрос на тему «Кому интересны онлайн‑курсы?», и увидел большую заинтересованность. Я и Aleksey Dolgushev за месяц проделали большую работу и подготовили интересный и объемный доклад. Уже в эту среду (завтра) с 12.00 до 13.00 будет сама презентация [Sravni Tech Meetup], я проведу ее удаленно для вас (30 минут сам доклад и 30 минут отвечаю на ваши вопросы). В докладе хочу поделиться опытом: за 5 лет я прошел (полностью) более 15 онлайн‑курсов; площадки: Coursera, Educator и TeachIn (МГУ). На встрече обсудим:
— Зачем вообще проходить онлайн‑курсы; какая от этого польза
— Демотиваторы, которые мешают людям проходить курсы
— Про полноценное онлайн‑образование удаленно от топовых ВУЗов мира
— Куда смотреть, где живут правильные курсы
— Как подобрать хороший курс
— Лайфхаки: как получить бесплатный доступ к платному контенту, как не бросить курс в процессе и другие советы
А теперь давайте поглубже поговорим о теории типов. Собственно, Роб в своей книге приводит 11 простых правил выведения типов, которые очень легко запрограммировать и на которых все построено. Он утверждает, что можно взять любой классический учебник по математике и полностью его алгоритмизировать. Любой ход мыслей любого математика, даже самого умного и сложного, можно представить в виде цепочки из N применений этих правил. Если вы взяли любой учебник по теории и не можете каждый его шаг транслировать в маленькие шаги и свести все к логике — то ваша подготовка недостаточно глубокая. Любой (достаточно глубокий) учебник математики = определения + выведение новых результатов на основе предыдущих + небольшое текстовое описание, которое можно выкинуть.
Список из 11 правил выведения типов, на которых все построено
Можете провести параллель с документацией Coq, в которой описано 19 правил выведения обычных типов и еще вот тут 4 правила для выведения индуктивных типов. Coq сильно расширил базовые правила, чтобы было удобнее сопровождать большие проекты по формальной верификации ПО, но при этом остался совместим с золотой классикой исчисления конструкций (Calculus of Constructions).
У читателя может возникнуть вопрос — почему именно 11 правил выведения типов? Может ли их быть меньше? Да, может, есть PTS (Pure Type System), которая стирает границу между термином и типом. Также, есть комбинаторная логика, в которой всего 3 символа (комбинатора) S, K и I. Было доказано, что любые правила выведения типов можно свести с этим 3-м комбинаторам и комбинациям из них. Если вы хотите особо подзапариться, то можете написать движок комбинаторной логики, в которой вы построите 11 правил выведения типов λD на основе этих комбинаторов, а на них уже дальше будете строить все остальное и делать упражнения из книги. Но, на мой взгляд, это уже оверкилл, тк 11 правил λD весьма просты к реализации и пониманию, а также на них основаны теорем‑пруверы Coq и Lean, так что имеет смысл брать именно 11 правил λD за основу.
Тут нужно также заметить, что на каждом этапе можно «срезать углы» и вместо того, чтобы выводить что‑то, можно просто заткнуть дырку аксиомой. Это очень плохо для обучения и глубины понимания, но нужно иметь в виду, что такой подход есть:
Вместо того, чтобы выводить правила и концепции математической логики из теории типов, можно просто накинуть десяток‑другой аксиом. Например, для конъюнкции (A ∧ B) будет 4 аксиомы — одна постулирует существование самой конъюнкции как типа, еще одна на основе A и B выводит (A ∧ B), а другие две на основе (A ∧ B) вытаскивают А и вытаскивают B. Если вы хотите по‑быстрому разработать свой теорем‑прувер на основе логики первого порядка, можете пойти по этому пути. Но лучше все‑таки разобрать правила выведения типов и на их основе все сделать.
Вместо того, чтобы выводить аксиомы Пиано (5 штук) из аксиом ZFC, можно просто их постулировать как аксиомы. Например, Терренс Тао поступает именно так в начале своей книги Analysis I, а иначе его книга могла бы увеличиться в полтора раза.
Вместо того, чтобы выводить всякие концепции типа «пара (a, b)», ее свойство и существование декартова произведения и из теории множеств, можно просто принять их как примитивные и добавить как аксиомы
Вместо того, чтобы выводить всю цепочку числовых систем (N → Z → Q → R), можно сразу же перейти к свойствам R и постулировать существование множества R и аксиомы на нем (поле + порядок + полнота). Многие курсы по математическому анализу именно так и поступают.
Любую слишком большую и толстую теорему в теории вероятности или статистике можно принять на веру и добавить, как аксиому. Собственно, многие курсы и учебники по статистике так и поступают для большинства теорем
Математиков можно поделить на 2 большие группы — алгебраисты и аналисты. Тут можно ссылаться на эксперимент с кукурузкой, в котором показали, что представители этих двух направлений едят кукурузку по‑разному. Мне кажется, что большая часть программистов в индустрии — это алгебраисты, а большая часть статистов/дата‑саентистов — это аналисты. Собственно, школьный предмет «Алгебра и начала анализа» знакомит с основами этих двух направлений. Когда я учился в школе, мне нравилось примерно 60% от того, что мы делали на школьной математике (алгебраическая часть), и я не любил другие 40% (аналитическая часть). Собственно, сейчас я как раз развиваю аналитическое мышление и надеюсь, что мои увлечения фундаментом математики помогут мне овладеть одновременно двумя этими направлениями и есть кукурузку так, как я захочу.
Мне всегда было интересно, как именно происходит переход от алгебраической формы (N = A ∪ ∅) к аналитической форме (p → q → r). На форумах (StackOverflow / Quora) писали, что вся математика может сводиться к небольшому набору аксиом и любое математическое высказывание можно трассировать в виде огромного дерева логических выводов (импликаций), но мне было непонятно, как именно алгебраическая форма вписывается в это дерево. Собственно, в главе 12 «Mathematics in λD: a first attempt» Роб Недерпелт раскрыл этот механизм и ввел йота‑дескрипторы. Получилось очень компактно и аккуратно, всего в 6 строчек вписалось. Он добавил их как 2 «псевдоаксиомы» (примитивные определения), но по сути они не являются аксиомами и не делают теорию типов логически сильнее (и это было доказано). То, что они реально делают — они добавляют «математический сахар» для тех математических объектов, которые (было доказано) существуют и уникальны. Например, вы можете доказать 1 раз, что существует пустое множество и притом только одно, назвать теорему empty_set_unique, и потом ссылаться на это множество через (ι _ (empty_set_unique)): Set. Далее, вы прячете эту йоту под термин ∅, и используете ее так, как ее принято использовать во всех математических текстах. Если вам понадобиться свойство пустого множества, вы можете развернуть термин ∅ обратно в йоту и из нее вытащить свойство.
Собственно, во всех классических математических текстах используют йота‑дескрипторы в неявном виде. Даже ваш школьный учитель математики использовал его много раз на доске, когда писал N и ссылался на уникальное множество натуральных чисел. Под ним прячется йота, а под йотой — доказательство существования этого множества и его уникальности.
Как выглядит йота-дескриптор и его свойство
Можно также посмотреть, как в стандартной библиотеке Coq определяются йота‑дескрипторы. По сути, там тоже самое, но усложненно через использование дополнительных определений и индуктивных типов. Для обучения и понимания\первого знакомства, это усложнение вообще не нужно и сбивает с толку. Это еще одна причина, по которой лучше обучаться по учебнику с акцентом на чистую теорию, а потом уже переходить к конкретной имплементации.
Еще один интересный и простой пример — что такое массив? Что вы видите, как программист, когда думаете о массиве [a, b, c], но без учета порядка элементов? Я всегда видел 3 ячейки в памяти (по 4 байта каждая), которые хранят переменные a, b, c друг за другом. А теперь, я вижу другое — я вижу логическое выражение ∃s. ∀x. ((x ∈ s) ⇔ (x = a ∨ x = b ∨ x = c))). А если учитывать порядок, то это будет функция (множество пар), которая проецирует множество {0, 1, 2} на множество {a, b, c}, т. е. ∃s. ∀p. ((p ∈ s) ⇔ (p = <0, a> ∨ p = <1, b> ∨ p = <2, c> ))). А пару, тоже можно выразить через множество. В общем, в IT все отлично формализуется.
Формализованную математику еще иногда называют механизированной математикой (mechanically checked mathematics). Если вам близок инженерный подход, можете представлять себе математику как огромный завод, на котором в качестве сырья выступает набор из 9 аксиом, а в качестве стандарта сборки — 11 правил выведения типов. Небольшие фабрики производят из этого сырья пруф‑объекты, и потом катят эти пруф‑объекты по ленте к другим фабрикам. Возможно, я переиграл в Satisfactory.
Тут надо еще заметить, что математику (исторически) принято изучать от конкретного к общему. Сначала нужно освоить исчисление (Calculus), понять его применения и выработать интуицию вокруг вычисления конкретных математических объектов и решения конкретных задач, а уже потом переходить к анализу вещественных чисел (Real Analysis). Тут можно ссылаться на провальный эксперимент New Math в США в 1970 году, когда попытались внедрить фундамент математики (теорию множеств и символическую логику) в школьную программу, и заменить ими унылое заучивание таблицы умножения\решение уравнений и так далее. Как выяснилось, это плохая идея — сначала нужно все‑таки сформировать некоторую грязную базу и потратить силы\время на нее (и это наверняка вызовет дискомфорт), а уже потом переходить к чему‑то более абстрактному и чистому.
А теперь поговорим о технических инструментах, которое реализуют внутри себя теорию типов и решают различные практические задачи. Начнем с Coq (он же The Rocq Prover). Он — классика в области формализации математики и формальной верификации ПО. Coq появился в 1984 году и занял эту нишу довольно плотно. Есть и более новый конкурент у Coq — это Lean. Но я не нашел достаточно мотивации, чтобы взять его с самого начала или перейти на него:
Lean построен на той же теории типов, что и Coq, а значит фундаментальных плюсов у него нет.
В документации по Lean я не нашел строгую формулировку правил выведений типов (которая есть у Coq), и это плохой знак.
Lean моложе Coq на 24 года, а значит сообщество и экосистема намного меньше, а также база решенных проблем и применений намного тоньше. Например, у реддита Coq 2500 участников, а у реддита Lean — всего 390.
В Coq вливает много денег большой государственный исследовательский центр во франции (INRIA), а Lean — финансирует небольшой исследовательский отдел Microsoft (но тут я могу ошибаться).
У Coq есть 6-томник «Software Foundations». Ради одного только его я мог бы выбрать Coq
Я выбрал Coq вместо Lean примерно по тем же причинам, по которым я когда‑то выбрал Java вместо С#. Но кроме Coq и Lean, есть и другие теорем‑пруверы. Isabelle/ZF и Metamath тоже все выводят из ZFC, но я их не выбрал в силу их малой популярности, а также слишком кастомного ядра и отсутствия строгой фундаментальной теоретический базы.
У нас есть 3 возможных уровня применения теории типов для формализация математики:
Уровень 1 — мы используем теорию типов только как движок для математической логики, а дальше про нее забываем и работаем полностью внутри математической логики и выводим все математические структуры из аксиоматической теории множеств. Этот подход самый трудозатратный, но он дает самый лучший результат для обучения и глубокого понимания. Поскольку моя цель — это как раз обучение и понимание, я придерживаюсь только этого подхода.
Уровень 2 — мы используем теорию типов не только как движок, но еще и перекидываем некоторые фрагменты теории множеств в нее. Результат получается намного более компактным и удобным для практических задач верификации, но не очень хорош для обучения. Например, вместо того, чтобы выводить множество натуральных чисел из аксиомы бесконечности, мы можем представить натуральные числа как индуктивный тип, или хитро ввести их через йоту. Таким подходом пользуется Роб Недерпелт в его главе по теории множеств, а также он используется в стандартной библиотеке Coq. Мне совсем не нравиться этот подход, так как он ломается на всяких штуках типа «как представить подмножество?» или «как представить множество всех подмножеств (powerset)?» и там приходится костылить.
Уровень 3 — мы полностью переходим в теорию типов и используем ее не только как фундамент для логики, но еще и как фундамент для математических структур. Тут можно отметить работу нашего соотечественника Владимира Воеводского, который развивал гомотопическую теорию типов и даже основал библиотеку Coq для нее. Но это исследовательская область, и у меня пока нет мотивации в нее погружаться. Она настолько не готова, что даже в начале учебника по гомотопической теории типов написано, что теория в процессе изменений и все может поменяться. Возможно, я когда‑нибудь посмотрю курс лекций по теории гомотопии и попробую разобраться, как именно она стыкуется с теорией типов и где это можно применить в моих задачах.
Если вам интересны конкретные применения Coq для решения реальных задач, то можно ссылаться на CompCert — полностью формально верифицированный компилятор языка С. Во время его формализации, исследователи нашли и поправили 100+ критических багов, и как результат — самолеты летают более надежно. Еще есть более свежий проект — CertiKOS, полностью формально верифицированная операционная система, которую невозможно взломать логическими методами. Ее формальная верификация заняла 1 миллион строк кода на Coq. Еще Coq используется в верификации всяких штук в инфобезе типа TLS‑протокола.
Работа по формальной верификации нейронных сетей тоже есть, и я уверен, что это направление будет очень сильно расти в ближайшем будущем. Люди очень боятся восстания машин, так что будут вливать много денег в то, чтобы сделать AI безопасным и надежным. Чтобы дать такую гарантию на 100% — нужны математические методы.
Если вас интересует ситуация в индустрии теорем‑пруверов в целом, то там все очень хорошо. Можно ссылаться на список из 100 самых популярных теорем и списка теорем‑пруверов, в которых они доказаны. Видно, что суммарно покрытие составляет 99 теорем из 100 — каждая из них покрыта хотя бы в одном теорем‑прувере, а на Coq приходится покрытие 79 теорем. Особое внимание можно уделить теореме‑доказательстве иррациональности квадратного корня, которая играет ту же роль, что и «чайник» в 3D графике для проверки движков, и все теорем‑пруверы ее доказывают. Также можно обратить внимание на теорему центрального предела (The Central Limit Theorem), которая покрыта только в теорем‑прувере Isabelle. Сложилось впечатление, что она играет очень важную роль в математической статистике и я пообещал себе, что не вернусь к учебнику по статистике, пока эту теорему не формализую и не пойму до конца, как она работает изнутри.
Еще можно упомянуть проект QED manifesto, цель которого — формализовать и компьюторизовать вообще всю математику. Пока что QED utopia не была достигнута, но максимально к ней приблизился именно проект Mizar Mathematical Library. Я думаю, в будущем к этому проекту вернуться и благодаря AI смогут достичь QED‑утопии. Можете почитать сам манифест, он написан довольно понятным языком и разбирает популярные заблуждения по поводу несовместимости логики, парадоксы и так далее. И аргументирует, что такой проект технически и логически достижим.
Я рекомендую всем, кто умеет программировать, пройти хотя бы первую главу первого тома «Logical Foundations». Она не требует специальной подготовки и займет у вас пару недель. В рамках этой главы, вы построите натуральные числа (N) на основе индуктивных типов, а также их базовые свойства (аксиомы Пиано), и базовые операции (сложение\умножение\возведение в степень\факториал). Также вы познакомитесь с принципом работы Coq и его базовыми тактиками.
Если вы — разработчик в индустрии, то вы, наверняка, привыкли писать императивные программы и лишь изредка использовать функциональное программирование. Хотя на некоторых работах может делаться акцент на функциональщине в силу специфики бизнеса и\или выбранного стека технологий. Например, мы в Edna используем проект Reactor и реактивный подход довольно часто, а на прошлых работах я часто применял Stream API. В случае Java у нас JVM и работа процессора является императивной по своей природе, а функциональное программирование эмулируется внутри императивной модели вычисления (RAM‑модели). А вот в индустрии теорем‑пруверов все наоборот — за основу взята теория типов на основе лямбда исчисления, которая является полностью чистой и функциональной. А императивный подход достигается путем введения языка тактик и автоматизации. Есть 2 способа программировать математические теоремы — напрямую через лямбды, а также через тактики, которые под капотом крутят эти лямбды. Любую теорему Coq можно представить в виде огромной мотни из лямбд. Команда «Show Proof.» печатает вам пруф‑объект (низкоуровневое доказательство теоремы). Coq правда любит прятать их, и нужно через небольшой лайфхак (Defined вместо Qed) определять теоремы, чтобы они не прятались.
Как выглядит доказательство правила Де-Моргана (¬(A ∧ B) ⇒ (¬A ∨ ¬B)) на самом низком уровне
fun (A B : Prop)(H : forall(_ : forall (C : Prop)(_ : forall (_ : A) (_ : B), C), C)(A0 : Prop), A0) =>exc_thrd A(forall (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C), C)(exc_thrd B(forall (_ : A) (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C),C)(fun (H2 : B) (H3 : A) =>H (fun (C : Prop) (h : forall (_ : A) (_ : B), C) =>h H3 H2)(forall (C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0,C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0,C), C))(fun (H2 : forall (_ : B) (A0 : Prop), A0) (_ : A)(C : Prop)(_ : forall _ : forall (_ : A) (A0 : Prop), A0, C)(H0 : forall _ : forall (_ : B) (A0 : Prop), A0, C)=> H0 H2))(fun (H2 : forall (_ : A) (A0 : Prop), A0) (C : Prop)(H0 : forall _ : forall (_ : A) (A0 : Prop), A0, C)(_ : forall _ : forall (_ : B) (A0 : Prop), A0, C) =>H0 H2)
Просвечивается exc_thrd — аксиома исключения среднего, через которую и идет доказательство (тк это правило в данной форме — не конструктивно). Других аксиом тут нет.
Собственно, fun — это лямбда и вводится через правило абстракции (abst). forall — это Π‑тип, выводится через (form). Prop — можно заменить на звездочку.
Напечатал путем выполнения команды Eval cbv in deMorganNotAnd. Вот таким нехитрым способом, можно для любой теоремы, доказанной внутри Coq, получить ее лямбда‑форму, развернув все определения.
Особый интерес представляет то, что все учебники из серии Software Foundations интерактивно читаются внутри IDE. Именно таким должен быть учебник математики будущего — на 100% механически формализован и верифицирован, подача учебного материала перемешена с упражнениями, а также есть среда выполнения и язык программирования, которые позволяют экспериментировать\проверять\выходить за рамки. Собственно, тут можно ссылаться на усилия Кевина Баззарда по внедрению теорем‑прувера Lean в имперском колледже Лондона в математические программы (The Xena Project). Я очень поддерживаю такие штуки и думаю, что математическое образование будет именно таким на всех уровнях.
Есть два способа изучать математику — от учителя к ученику (классический подход), а также с компьютером и без учителя (новый подход). Конечно, было бы круто, если бы хорошие учителя были бы доступны по всем предметам, а ученикам было бы приятно и интересно проводить время с ними. Но на практике, есть огромное количество проблем у этого подхода. Они не только финансовые (хороший репетитор\ментор будет очень дорого стоить), но и привязаны к месту проживания (не всегда можно в принципе кого‑то найти в доступности). А также очень трудно найти кого‑то, с кем вам приятно и комфортно проводить время, чтобы человек вам нравился. По итогу, приходится развивать альтернативные направления. Одно из таких направлений — смотреть онлайн‑курсы и видео, в которых у вас создается впечатление, что лектор общается с вами, и вы параллельно с ним прорешиваете задачи, как с репетитором. Другое направление — это всякие интерактивные среды и компиляторы\песочницы, которые строго ограничивают ваши действия и дают информативные сообщения об ошибках, если вы что‑то делаете не так. В этом смысле, теорем‑пруверы типа Coq являются «идеальным учителем» математики, который видит 100% ваших ошибок в логике и просто не даст вам двигаться дальше, если что‑то сделано не так.
У меня есть гипотеза о том, что во время занятия (реальной) математикой у человека в голове формируется что‑то типа теории типов на уровне нейронов. Я пока не могу подтвердить мои догадки и ссылаться на исследования из области нейронауки, но я верю в эту гипотезу и уверен, что в будущем что‑то подобное будет экспериментально доказано.
Еще один лайфхак — если вы девушка и очень хотите войти в айти, то вы можете попробовать пожить с мужчиной, который работает программистом в айти компании (но не со мной) пару лет вместе. Если вы будете каждый день общаться на бытовые темы, вы будете перенимать ход мыслей и впитывать базовые идеи, даже если он вас не будет обучать в явном виде. Это супер‑важно и может сильно вам помочь в развитии потом освоить язык программирования или профессию QA\HR. Но даже если вы ничего не освоите, у вас все равно есть шанс пробиться в айти на большую зарплату. Я периодически встречал коллег, которые ничего не знают\не умеют, но думают как знающий\умеющий человек (мимикрируют под программиста) и хорошо умеют проходить собесы.
А если вы мужчина, то ждите появления виртуальных учителей\менторов на основе GirlfriendGPT, они помогут вам решить главную проблему в образовании — проблему с мотивацией.
А теперь поговорим о теме «войти в IT». Главная причина, почему обычные люди не могут комфортно войти в айти и научиться программировать — это отсутствие математической подготовки и трудности с ее получением. Вот вам секрет, как сделать из обычного человека хорошего программиста: нужно потратить пару лет на школьную математику и подтянуть ее до уровня физ‑мат школ, а уже после этого переходить к языкам программирования. А сразу прыгать на курсы или онлайн‑системы типа JavaRush без уверенной математической базы — это очень плохая идея.
Если вам интересно, откуда я насобирал столько полезной информации по теме фундаментальной математики и связал все воедино, я могу раскрыть мои источники. Я уже 8 лет как активно использую английский Гугл (почти каждый день) и много с ним общаюсь на разные темы. Он дает мне ссылки на английскую википедию, а также на всякие сайты типа MathOverflow, Quora и Reddit. В 2024 ChatGPT созрел как замена Гуглу, поэтому в декабре я купил подписку ChatGPT Plus и перешел на него в качестве дефолтового поисковика в Chrome. Я планирую в 2025 полностью отказаться от Гугла и пользоваться только ChatGPT, переписываясь (или общаясь голосом) с ним на английском языке.
А теперь поговорим о списке практических применений фундаментальной математики. Список довольно большой и он только растет, у меня появляется все больше и больше разных креативных идей каждый месяц. Кажется, у меня все расписано на ближайшие 10 лет и все мое развитие и рост в будущем (как личный, так и профессиональный) будут затрагивать теорию типов\теорию множеств\теорем‑пруверы.
Применение #1: Войти в AI/ML и сделать это по‑царски. По опыту с компьютерными науками я знаю, что чем глубже подготовка по теории — тем лучше. Это не только входной порог, но еще и задел на развитие, более широкий выбор из компаний, возможность миграции внутри компании, гибкость в развитии и резистентность к сокращению. Где‑нибудь в 2026–2027 году я буду готов и сразу возьму какие‑нибудь крутые курсы с Курсеры или MIT OpenCourseWare по AI. Совсем не обязательно полностью формализовать весь фундамент под AI/ML. Я думаю, что глубокое понимание и формализация некоторых ключевых теорем в анализе и теории вероятности будет более чем достаточно.
Применение #2: Алгоритмы и структуры данных, их анализ и формализация. Собственно, я уже итак довольно глубоко проработал эту область и прошел 2/4 курса из специализации на Курсере по дизайну и анализу алгоритмов от Стендфордского университета в 2022 году. Моя главная цель — это не только комфортное прохождение алгоритмических собесов и сильная позиция на рынке, но еще и возможность брать более крутые и интересные задачи. Я пока не знаю, как именно буду продвигаться дальше, но я точно знаю, что хочу формализовать машину Тьюринга внутри ZFC и научиться ее там крутить, а также разобраться, как именно RAM‑модель (математический ассемблер) компилируется в машину Тьюринга. Если это сделать, то можно добиться 100-го понимания самой концепции алгоритма и, как результат, получить большой бонус к решению алгоритмических задач. Будет идеально, если я смогу на LeetCode решать алгоритмические задачи одновременно на двух языках — математическая модель и доказательство корректности\сложности на Coq, и быстрая имплементация алгоритма на Java.
Входной порог в алгоритмы и структуры данных - что требуется знать
Взял из CLRS
Тут еще надо заметить, что среди программистов в России очень много слабых IT‑специалистов с очень слабой математической подготовкой, которые решают весьма рутинные и неинтересные задачи в проектах с кодовой базой плохого качества, а также не хотят изучать что‑то новое и вкладываться в развитие. Такой путь развития и раньше был не перспективен, а теперь (с учетом изменений в мире AI) кажется совсем провальным и я вам крайне не рекомендую прислушиваться к мнению таких знакомых, если они у вас есть.
Применение #3: Формализация программного обеспечения. Как я уже писал, Coq активно используется в индустрии для того, чтобы доказать корректность работы программ и вообще любых IT‑систем. Я изначально думал, что это слишком узкое направление и в целом не очень полезное для карьеры Java‑разработчика. Сейчас я так не считаю. В моей работе регулярно встречаются ситуации, которые критически важны для бизнеса и которые прямо таки напрашиваются, чтобы их формализовали. Формализация позволит не только дать более четкий\аргументированный ответ бизнесу (актуально для техлида), но и предотвратить инцеденты на проде (и отдыхать вместо того, чтобы их исправлять). Например, микросервисное взаимодействие и некоторые архитектурные паттерны прямо так и напрашиваются, чтобы их формализовали. Компании тратят куча денег и ошибки — стоят очень дорого. Лучше убедить бизнес, чтобы эти деньги положили Java‑разработчику в карман.
Собственно, я полтора года назад прорешал первые 6 глав на 100% в учебнике Logical Foundations, но застрял на главе «Inductively Defined Propositions», тк она (по всей видимости) — повышенного уровня сложности. На тот момент у меня не было такой глубокой теоретической подготовки, как сейчас. Сейчас я могу вернуться и закончить первый том. В ближайшие пару лет сделаю, если не будет более интересных приоритетов.
Применение #4: Формализация баз данных. Базы данных используют вообще все специалисты в IT (даже менеджеры), и возникает очевидный вопрос — а как формализовать реляционные БД? В 2021 году я наткнулся на очень крутую книгу Applied Mathematics for Database Professionals by Lex deHaan, в которой авторы очень чисто формализуют современную БД и язык SQL в терминах математической логики и теории множеств. Эта книга была для меня большим открытием и я довольно быстро и комфортно прорешал первые 8 глав и упражнения к ним на бумаге. Она не только покрывает простые CRUD‑операции, но и более сложные темы, такие как структура БД, ее ограничения и транзакции.
Собственно, это очень полезно для более глубокого понимания логической сути БД (что в БД важно, а что второстепенно), помогает не утонуть в деталях имплементации конкретной БД, а сконцентрироваться на ключевых моментах и более грамотно проектировать БД.
Пример Select и его формальная форма на языке теории множеств
select distinct e.JOB from EMP e where e.MSAL > 4800 or e.SGRADE >= 6
Входной порог в теорию БД - что требуется знать
Применение #5: Развитие в менеджмент. У меня сложилось впечатление, что хорошие менеджеры (особенно топ‑менеджеры) — это весьма образованные люди и они максимально используют математику в работе. Речь идет не только о простом статистическом анализе данных, но еще и о построении и проверке гипотез, использовании инструментов Data Science, а также применении всяких интересных штук типа Теории Игр/Теории оптимизации/Линейного программирования для принятия крупных стратегических решений. Собственно, можно попробовать развиваться по этому пути и заработать очень много денег, которые многократно окупят затраты на фундаментальную математику. Можно также попробовать соединить теорию менеджмента, сертификацию PMP и генеративные нейронные сети, чтобы сделать что‑нибудь интересное и креативное.
Тут я хочу заметить, что среди знакомых я встречал много примеров плохих менеджеров — которые уходят в менеджмент из‑за профессиональной деградации и лени, получают зарплату сильно меньше хорошего программиста, а также используют весьма примитивные инструменты и личный (иногда эмоциональный) опыт в принятии решений. Такой путь развития я в принципе не рассматриваю, и под словом «менеджер» я подразумеваю именно математического менеджера, которого я описал в абзаце выше.
Применение #6: Разработать свой 3D движок и свою 3D игру. Я начал программировать в 13 лет с разработки своих игр и 2D движков для них в 2007 году. С тех пор я мечтаю попробовать разработать свою 3D игру — как хобби и для удовольствия. Мне все равно придется глубоко осваивать линейную алгебру для ML, а в качестве бонуса и мотиватора можно сделать свой 3D движок с полного нуля и с полным пониманием фундамента.
Применение #7: Глубоко понять доказательную медицину. У меня сложилось впечатление, что лучшая часть медицины — это та, что базируется на математической статистике. И медицина будущего будет именно такой, ее нужно полностью свести к статистике и теории вероятности. Мне очень интересно это направление и ради только его одного я мог бы потратить пару лет на обучение. Математика может не только помочь интуитивно понять сложные исследования и статьи в медицине, но еще и попробовать всякие интересные проекты, типа Hummod (cамая полная математическая модель физиологии человека из когда‑либо созданных).
Применение #8: Глубоко понять, как устроен реальный мир на низком уровне. У меня еще со школы сохранилась мечта — написать программу, которая из законов квантовой физики выводит таблицу Менделеева и предсказывает химические реакции, а также закладывает фундамент химии. Но на тот момент, у меня не хватало ни алгоритмов, ни глубокого понимания квантовой физики и ее математической базы. Собственно, в ближайшем будущем я могу попробовать освоить и формализовать дифференциальные уравнения и дальше сделать что‑то типа симулятора квантового мира. Но когда у меня до этого руки дойдут — не знаю. Сейчас мне 31 год, и столько всего нужно изучить и попробовать, много других приоритетов есть. Возможно, когда мне будет 50+, я вернусь к этому вопросу.
Применение #9: Написать убер‑диссертацию на тему математического фундамента ChatGPT. Собственно, я уже учился в аспирантуре ИТМО (2017 — 2020) на кафедре информатики и прикладной математики (ИПМ), но на тот момент у меня не было реального исследовательского проекта, так что я сдал академический минимум и ушел. По мере накопления математического фундамента, я понимаю, что он идеально подходит для написания диссертации. Будет круто, если у меня реально получится пройти весь путь от теории типов до теории генеративных нейронных сетей и получить PhD в этой сфере. Но когда у меня на это появится свободное время — я не знаю. Я думаю, что скорее восстание машин начнется, чем я успею защитить диссертацию...
Моя главная цель при написании этой статьи — получить как можно больше отзывов и обратной связи и скорректировать\дополнить\расширить мои планы на будущее. Буду рад услышать ваши замечания, рекомендации, советы и критику. Чем больше напишите, чем лучше. Можете писать в комментариях, на почту (kciray8@gmail.com) или в Телеграм личным сообщением.
