Карта математики | Maximatika

🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 3. Аксиома унивалентности ❤️Начнём с самого сердца. 💭Помните в позапрошлом посте мы заявили в качестве одной из проблем использования теоретико-множественных основ в мире компьютерных доказательств - огромное количество лемм о переносе свойств вдоль изоморфизмов (далее буду использовать более широкое понятие эквивалентности) . Простой пример: тип BOOL и условный тип BIN {0,1} очевидно эквивалентны друг другу - в них явная биекц...

Soon...

А вот и новый сезон!🎉 https://www.youtube.com/watch?v=0EkY9nq0bGg 🎥В прошлой серии видео мы заложили некоторую интуицию о том, что такое математика. Установили удобную нам фундаментальную теорию и испытали её на прочность. 🦸‍♂️Итак, встречайте - герой нашего нового сезона - теория множеств. 🥇Несмотря на то, что в последнее время перспектива несколько изменилась и как мы знаем появились альтернативные основания математики гораздо более общие, чем теория множеств. Пока еще именно она, чаще все...

🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 2. Становление унивалентных оснований 🏛 Идея логических оснований витала в воздухе ещё с конца XIX в. Начиная с работ Фреге, пытавшегося показать, что арифметика может быть полностью выведена из логики. Затем воодушевленное начало XX в. — программа Гильберта, Principia Mathematica Рассела и Уайтхеда. 📉Но уже в середине XX в. после работ Гёделя интерес подостыл и сформировалось мнение, что программа логических оснований, хотя и...

🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 1. Почему не теория множеств? ❓Каким должен быть фундамент математики, пригодный как для человеческого мышления, так и для компьютерной верификации? По мнению Воеводского он должен включать следующие три компонента. 1) 🧾 Формальная система вывода Язык + правила вывода. Полностью формальные, так что корректность записи доказательства может быть проверена компьютерной программой. 2) 🧠 Семантический слой Придаёт смысл предложения...

🧠📚Предлагаю на этот раз поговорить об идеях Владимира Воеводского. Тем более это напрямую связано с фундаментальными основами математики. ❓ Что побудило его развивать новые основания и чем ему не угодили уже имеющиеся? ❓ А также, можно ли доверять компьютерным проверкам доказательств? Сегодня немного предыстории... 📜 Лекции в IAS (Institute for Advanced Study) и первая трещина в доверии Все началось в 1999 - 2000 годах, когда Воеводский читал цикл лекций в IAS и Пьер Делинь (профессор математ...

7️⃣А вот и последнее видео ... этого сезона🎉 https://www.youtube.com/watch?v=T11wiDsg2vI В прошлом видео мы наконец выбрали подходящий нам фундамент математики - теорию множеств. Она простая для восприятия, интуитивная и достаточно мощная, чтобы предоставить универсальную основу для формализации математических теорий. Но все оказалось не так просто. 💪Сейчас ей придется пройти проверку на прочность. Сегодня мы поговорим про парадоксы, так или иначе связанные с теорией множеств, логикой и языком...

🌊🔢НАВЬЕ—СТОКС и ПРОБЛЕМА ОСТАНОВА. Часть 3. Связь 🌊Навье-Стокс: 3-мерные уравнения, описывающие поведение вязкой несжимаемой жидкости. 🔢Проблема останова: Существует ли универсальный алгоритм, определяющий для данного описания процедуры и её начальных входных данных, завершится или нет выполнение этой процедуры. 🧩Теперь соединяем: 🟦Входные данные - начальное положение частицы в потоке; 🟧Программа - сама структура потока; 🟩Результат вычисления - некое событие (конечное положение частицы, ...

🌊🔢НАВЬЕ—СТОКС и ПРОБЛЕМА ОСТАНОВА. Часть 2. Вычислимость в физических системах В прошлом посте мы поженили гидродинамику и вычисления. Близко к цели, но пока еще не прямая связь с проблемой останова. Чтобы приблизиться ещё на один шаг нам нужны не простые жидкостные вычислители, нам нужен аналог универсальной машины Тьюринга. 💬На самом деле Теренс Тао был далеко не первым, кто пытался связать физические системы с универсальными вычислителями. Как писал Р. Пенроуз в своей книге Новый ум короля...

С наступающим Новым годом!!!🎉