🧠📚Предлагаю на этот раз поговорить об идеях Владимира Воеводского. Тем более это напрямую связано с фундаментальными основами математики. ❓ Что побудило его развивать новые основания и чем ему не угодили уже имеющиеся? ❓ А также, можно ли доверять компьютерным проверкам доказательств? Сегодня немного предыстории... 📜 Лекции в IAS (Institute for Advanced Study) и первая трещина в доверии Все началось в 1999 - 2000 годах, когда Воеводский читал цикл лекций в IAS и Пьер Делинь (профессор математического факультета) делал записи и проверял каждый шаг его рассуждений. Только тогда обнаружилась ошибка в одной из ключевых лемм. 🗓А ведь прошло почти 8 лет с момента её доказательства! Хотя за всё это время несколько групп математиков изучали её на семинарах и использовали в своей работе, никто из них не заметил ошибки. И это явно не было случайностью. Техническое рассуждение авторитетного автора, которое трудно проверить и которое на первый взгляд выглядит, как верное, практически никогда не проверяется детально. ⚔️Критика Симпсона Примерно в то же время Карлос Симпсон отправил критику статьи (“∞-Groupoids and Homotopy Types”), опубликованной Воеводским совместно с Капрановым. Но он не смог указать, где именно в статье была ошибка, только утверждал, что построил контрпример. Из-за чего без дополнительных проверок было неясно, допущена ли ошибка где-то в статье или где-то в контрпримере. 🤝 Репутация и взаимное доверие Математические исследования опираются на сложную систему взаимного доверия, основанную на репутации, поэтому критика Симпсона не получила поддержки в математическом сообществе перед уже признанными в то время Воеводским и Капрановым. И дополнительных проверок не проводилось. А в 2013 году оказалось, что он был прав и ошибка была именно в статье. 🛤 Альтернативные пути проверки доказательств Все эти события всё больше утверждали Воеводского в мысли, что математическое сообщество не способно быть однозначным гарантом математических доказательств. Уж очень большое влияние имел человеческий фактор и необходимо было искать другие пути. “У меня не было инструментов, чтобы исследовать те области, куда меня вело любопытство, и те области, которые я считал ценными, интересными и красивыми.” 💻Лучшим решением казалось использование компьютеров для верификации математических рассуждений и логических построений. Но была одна проблема - основания математики не были готовы к решению этой задачи. Об этом в следующем посте...