Когда математики в ступоре и про важность софт-скиллов

 Публичный пост
28 ноября 2022  3497

Эта история не новая, завязалась она в 2012-ом и, как кажется, развязалась – в 2018-ом. Кто следил за историей доказательства abc-гипотезы, тот знает, о чем речь. Для остальных поведаю этот математический триллер, от которого любители математики могут почувствовать настоящий фриссон – тот самый мороз по коже.


Для тех, кто может испытать такое не только от музыки, но и от математики. Картинка отсюда.

Оговорка. Этот пост – комбинация нескольких других и щепотка моих рассуждений на тему. Также это версия с картинками моего поста в телеграм-канале "New Yorko Times", где я пишу про машинное обучение, карьеру, науку и прочие интересности (блог, к слову тоже есть https://yorko.github.io/).

ABC-гипотеза – одна из главных в теории чисел, она связывает сложение, умножение и простые числа где-то на “самом низком уровне”. В английском “conjecture” означает, что большинство верит в верность утверждения, но оно еще не доказано (в переводе на русский эта коннотация теряется, гипотеза – это всего лишь гипотеза). Я не буду тут играть в тру математика, смысл abc-гипотезы я не смогу толком оценить (после доклада декана ФКН Аржанцева по алгебраической геометрии я даже бабушке перестал говорить, что математик). UPD: суть гипотезы поясняется в еще одном научно-популярном посте на эту тему. Но важность abc-гипотезы можно оценить по вторичным признакам: во-первых, она еще не доказана, а значит, скорее всего с помощью существующих математических аппаратов ее либо невозможно либо очень сложно доказать (вряд ли уж за почти 40 лет человечество проглядело простое элегантное доказательство, хотя как знать). Когда наконец будет доказана, значит, математика скорее всего выработает принципиально новый аппарат и продвинется далеко вперед. Во-вторых, как говорят математики, великая теорема Ферма – просто следствие abc-гипотезы, значит, если доказать abc-гипотезу, то можно “дешево” получить доказательство пресловутой великой теоремы Ферма, формулировку которой поймет любой школьник, а на доказательство которой понадобилось более 350 лет человечества и несколько лет затворничества одного конкретного человека – британца Эндрю Уайлса.


Синъити Мотидзуки. Фото: университет Киото.

И вот в 2012 году японец Синъити Мотидзуки выкладывает 4 статьи объемом более 500 стр. в сумме и утверждает, что доказал abc-гипотезу. Первая статья под названием «Интер-универсальная теория Тейхмюллера 1: Построение театров Ходжа», начинается с утверждения, что цель работы в «разработке арифметической версии теории Тейхмюллера для цифровых полей ограниченных эллиптической кривой… с помощью применения теории полуграфов анабелиоидов, фробениоидов, эталь тета-функций и логарифмических оболочек». Звучит как что-то на марсианском. Причем не только для нас, но и для специалистов. «Смотря на неё, ты чувствуешь будто читаешь статью из будущего или далёкого космоса», – написал в своем блоге Джордан Элленберг, профессор математики в Висконсинского университета. К слову, сервис ExplainPaper.com у меня поломался, когда я попросил Эй-Яй пересказать смысл аннотации первой статьи из серии.


Аннотация первой статьи из серии. Источник.

Сообщество математиков было в полнейшем ступоре. Игнорировать статью не получалось: Мотидзуки к своим 43 годам уже добился всего чего можно в математике, в 16 лет он поступил в университет Принстона, а в 22 года уже получил докторскую степень под руководством лауреата Филдсовской премии в области алгебраической геометрии Герда Фальтингса. Но и вникнуть в доказательство было почти невозможно: Мотидзуки цитирует в основном себя самого, в статьях, цитирующих опять же Мотидзуки, и т.д. по рекурсии – получается гора из почти 2000 статей. Лучшие умы алгебраической геометрии оценивали, что им нужно около года вникать в теории Мотидзуки, чтоб хотя бы сформировать хоть какое-то мнение о его теории. Не помогало и то что Мотидзуки не очень спешил пояснять свои “театры Ходжа” и прочие головоломные исхищрения, его не раз приглашали в топовые универы с курсами лекций, но японец довольно высокомерно отказывался, считая, что ни за неделю, ни за месяц нельзя объяснить его доказательство.

И получается патовая ситуация. Труд математиков могут оценить только математики (peer review), но в данном случае верификация слишком сложна, как будто подрываются сами основы самой, казалось бы, точнейшей и чистейшей из наук – математики. А пока лучшие умы вникают в новую статью, нам простым смердам остается только гадать, что происходит, надо ли гению распинаться и пояснять свои выкладки или мы, человечество, поймем все веке эдак в 24-ом, пусть лучше гений тем временем еще дальше продвинет науку.

Как вы уже наверное догадываетесь, так оно не должно работать. Наука – явление социальное. И автор исследования должен помогать людям понять себя, иначе – рискует быть непонятым и непризнанным. К слову, доказательство теоремы Ферма Эндрю Уайльзом тоже было очень сложным – специально наняли 7 математиков, которые около 2х лет только этим и занимались, что изучали доказательство Уайльза, а тот всячески помогал. Даже доказательство гипотезы Пуанкаре Перельманом, каким бы сложным ни казалось, было “нормальным”, потому что Перельман, несмотря на свой пещерный видок – нормальный ученый, действующий по устоявшейся конвенции, и смотрел он вдаль, стоя на плечах гигантов, а не соорудив Эверест из записанных в блокнотах только ему понятных мыслей.

По состоянию на 2013 год эта история прекрасно описана в статье “Парадокс доказательства на Хабре (перевод статьи “The paradox of the proof” выпускницы Стэнфорда Caroline Chen), советую почитать и комментарии на Хабре.

Развязка случилась только в 2018 году (вот статья в Nature про разоблачение). Два блистательных математика нашего поколения – немцы Jakob Stix и Peter Scholze приехали на неделю в университет Киото, чтобы разобраться с помощью Мотидзуки в его доказательстве. Вскоре после этого они объявили, что в доказательстве Мотидзуки – серьезный недочет, который нельзя быстро и просто пофиксить. Мотидзуки все отвергал. Кто прав? Что остается делать нам, тварям дрожащим? Только судить по вторичным признакам, а судя по ним, "ABC is Still a Conjecture". Попросту говоря, не сумев атаковать мысль, Мотидзуки стал атаковать мыслителей, совершая один за другим выпады в сторону немецких математиков и пытаясь доказать, что те ничего не поняли. К слову, спустя несколько месяцев после начала этих разборок, Peter Scholze получил Филдсовскую премию.


Немецкий математик, обладатель Филдсовской премии Peter Sholtze. Источник: Spiegel.

Что ж, поведение гениального японца в данном случае – красный флаг, можно смело утверждать, что теперь никто не будет всерьез воспринимать доказательство abc-гипотезы в исполнении Мотидзуки. Сообщество математиков отправило свой “десант” для проверки работ Мотидзуки, спасибо и на этом, все остальные, так же как и мы, судят о верности доказательства по вторичным признакам – поведению участвующих лиц.

Может ли доказательство Мотидзуки все еще оказаться верным? Может, но это очень маловероятно. Интересно пофантазировать и представить, что Мотидзуки мог бы ответить на критику блистательных немцев и выкрутиться красиво, но теперь это все уже теория.

Если спуститься с небес на землю и подумать, чему эта история может нас научить, то, пожалуй, это опять про тех пресловутых “токсичных гениев” (brilliant jerks) и софт-скиллы. Говорят, что корпорации сошлись во мнении что найм токсичных гениев того не стоит, важнее атмосфера в коллективе. Вот и тут гениальный японец проиграл уже по софт-скиллам: не играя по принятым правилам, ты вряд ли победишь, наука в целом и даже математика в частности – это деятельность социальная. Впрочем, я верю в то, что и по хард-скиллам Мотидзуки проиграл, а замечания Stix и Scholze действительно существенны и поэтому доказательство неверно. Наконец, хочется верить в бритву Оккама и в то, что доказательство abc-гипотезы должно быть простым – не Эверестом из статей, полностью понятных одному только их автору.

54 комментария 👇

Очень круто.

Всегда задавался вопросом, чтобы использовать математические абстракции на таком высоком уровне, нужен специально заточенный под это мозг?

Или это развивается теорией о 10000 часов?

  Развернуть 1 комментарий

@8l1iUcE6ChZrwkvYLiadov, мне отзывается дихотомия Джека Дэниелса в "от 800 метров до марафона". Есть талантливые люди, а есть обделенные талантом. Также есть лентяи и работяги. Два бинарных признака дают 4 комбинации. Дэниелс интересно рассуждает о талантливых лентяях и бездарей-работяг в контексте бега. Но если обратно к этим диким математическим абстракциям, уверен, это талантливые работяги – тут и гениальность нужна, и 10000 часов. Тот же Мотидзуки, как говорят, потрясающе работоспособен, может погружаться на многие часы без перерыва.

  Развернуть 1 комментарий

@8l1iUcE6ChZrwkvYLiadov, у меня всегда было ощущение, что если кто-то не понимает что-то из математики — значит он просто пропустил какой-то уровень, который позволяет это понять. Если закрыть этот пробел, то всё станет легко.

То есть математику можно изучать исключительно линейно, сначала концепцию счётных чисел, потом ноль, потом отрицательные числа. Без отрицательных чисел невозможно понять вычитание. А чтобы понять деление — надо разобраться сначала с действительными числами. Ну и так далее, каждое следующее знание становится гораздо более комплексным и сильно наслаивается и зависит от предыдущего. Если некуда наслаиваться — ничего не поймёшь.

Так что я уверен что математикой может заняться каждый, лишь бы прошёл весь путь от начала до нужного уровня

  Развернуть 1 комментарий

@iDeBugger, вопрос ведь был про абстракции на таком высоком уровне, а не про то, для каждого ли математика или нет. Мое мнение: чтоб понять, что за театры Ходжа и анабелоиды, о чем вообще этот японец говорит, недостаточно просто 10к часов вложить.

  Развернуть 1 комментарий

@yorko, ну да, наверное я не совсем корректно выразился. Я имел ввиду, что это в целом достижимо для кого угодно, а не какой-то специально заточенный мозг

  Развернуть 1 комментарий

@iDeBugger, я не думаю, что театры Ходжа и анабелоиды достижимы для кого угодно, мне вот как раз кажется, что нужен "специально заточенный мозг". Философский вопрос, конечно. Но кухонное рассуждение такое: 10к – это много, конечно, но это ресурс, которые есть у очень многих. И есть миллионы людей, которые могу выделить 10к часов на освоение математики на нужном уровне. Допустим, 10к человек (с потолка взял) реально выделили эти 10к часов каждый. Но вот почему-то Уйальзы и Перельманы все же единичны, а abc-гипотеза все еще не доказана и прочие задачи из списка университета Клея тоже не решены. Значит, просто закидать вопрос человеко-часами не получается, нужен еще талант.

  Развернуть 1 комментарий

@yorko, согласен про философичную природу вопроса :D

Дополню ещё, что есть вопрос эффективности приложения этих 10к часов, на мой взгляд. Поэтому мне не очень нравится формулировка про 10к часов. Просто влить 10к часов и правда не помогает.

Я бы сказал, что талант выражается в конкретных действиях: повышенный интерес к предмету, всё время поиск нового в предмете, попытки экспериментировать и выйти за рамки. Вот если бы мы могли как-то влить не просто 10к часов, а 10к часов людей с описанными выше признаками в отношении математики, вот это было бы эффективно.

У меня есть ощущение, что вот это и отличает принципиально Перельмана от, простите, среднего математика. Ну и наверняка случайность тоже играет роль.

  Развернуть 1 комментарий

@iDeBugger, если мы говорим о простой математике, а таковой наверное можно назвать условно всё изобретённое до 1900 года, то да.

Объяснения роляют. Я по приколу восьмикласснице-гуманитарию объяснял предел по эпсилон-дельта на 1 курсе. Объяснил за 10 минут. У меня самого на понимание ушло полтора месяца и много гугла и копания в учебниках. Уравнения объяснял четырёхлетней сестре, которая только научилась в базовое сложение и вычитание, закрывая одно из чисел сердечком и предлагая угадать. Двойной интеграл мы все проходим в 1 классе, когда нас просят посчитать площадь по клеточкам.

Опять же, математика это в значительной степени язык, а мозг у нас заточен под язык. Ребёнок в 4-5 лет понимает рекурсии и что только не, не прикладывая к этому никаких усилий.

Правильный порядок — тоже роляет.

Бывает ли талант к математике — не знаю.

  Развернуть 1 комментарий

@8l1iUcE6ChZrwkvYLiadov, @iDeBugger, то же самое можно сказать про программирование :) казалось бы, ну что там такого сложного, все постепенно строится из кирпичиков. Но далеко не все способны к такой деятельности даже на низком уровне.

ИМХО тут вопрос не в устройстве мозга, скорее должен быть интерес. А интерес - это скорее настройка мозга, чтобы определенная деятельность приносила удовольствие.

Еще должна быть возможность к сильной концентрации (привет людям с СДВГ)

Еще есть такой момент, как эффективные ментальные приемы (про которые почти никогда не говорят)

У меня в школе была большая проблема с орфографией. Все эти проверочные слова и т.д. не помогали. Несмотря на занятия с репетитором я постоянно делал ошибки в словах, и проверка диктантов была для меня мучением. Все изменилось, когда я в какой-то книжке вычитал, что можно просто запомнить визуально написание слова (как картинку). После этого все проблемы быстро исчезли.

Явно математики как-то хитро себе представляют все эти абстракции, а нам не рассказывают (не могут наверное :) )

  Развернуть 1 комментарий

@orbit, согласен, тоже считаю, что не все способны программировать, также как и математикой заниматься.

  Развернуть 1 комментарий

@yorko, ммм, я скорее хотел сказать обратное :)

Я достаточно длительное время считал, что соображаю средне. Но чем больше живу, тем больше поражаюсь, что оказывается соображаю я намного лучше среднего человека (ну там что-нибудь сложное запрограммировать, разобраться в какой-нибудь незнакомой предметной области и сделать в ней проект, научиться чему-нибудь новому по книгам). Это оказывается редкое умение.

При этом, мне не кажется, что мой МОЗГ работает как-то лучше среднего. Я считаю, что в идеальном мире, можно так сформировать учебный курс, что любого человека без отклонений в развитии научить чему угодно. Пробудить в нем интерес, изложить базу простыми словами, медленно двигаться, мотивировать и тестировать каждый шаг. Гениальным он может и не станет, но хорошего специалиста я думаю можно получить.

У меня как-то давно был такой эксперимент, я женщину 50 лет, которая работала всю жизнь переплетчицей, пытался научить работать на компьютере (что-то простое, вида "обведите мышкой эту линию"). Так вот, эксперимент с треском провалился )))

Причем проблема была не в том, что она плохо соображала или ей не хватало усидчивости, проблема была в том, что эта деятельность для нее была слишком новая (она никогда не работала на компе и не играла в игры и не училась).Это слишком сильно отличалась от привычного ей. Ей прямо физическую боль причиняла необходимость разбираться в компьютереных премудростях, хотя изначально она горела желанием переквалифицироваться, ведь дома за компом сидеть куда легче, чем стоять на ногах 10 часов и дышать вонючим клеем.

В целом, мне кажется, если бы я организовал обучение в игровой форме, разбил на мелкие-мелкие этапы, платил за выполнение каждого этапа, то в конце-концов можно было бы ее научить. Ну т.е. проблема не в мозге, а в его установках (у меня не получается, это слишком новое, мне не интересно, это не для меня и т.д.), т.е. люди сами себя ограничивают.

  Развернуть 1 комментарий

@orbit, понял, спроецировал ваше первое сообщение на свой мозг и сделал свой собственный вывод :)

Да, знакомо, напоминает, как я маму 3 года учил эсэмэски набирать, а Одноклассники она освоила за пару часов, поскольку подруги уже ранее освоили - был стимул не тупить.

Возможно, есть такие педагогические техники, чтоб и моя мама поняла доказательство Мотидзуки, но очевидно, они нами еще не открыты.

  Развернуть 1 комментарий
Марат Ямалиев мечтаю закрыть все тикеты 30 ноября 2022

А в какой момент "мороз по коже"? Математик не смог адекватно ответить двум проверяющим, конец истории.

  Развернуть 1 комментарий

@marat_y, все субъективно

  Развернуть 1 комментарий

@marat_y, в момент осознания что прямо сейчас делается наука. В момент когда оказывается что признанный математик может ошибаться со своей супер-теоремой. Да десятки их же, ты чего! Так то и Холмс из-за неправильного ТЗ на сотне с лишним страниц песеля на болотах ищет. Да и музыка, от которой "мороз по коже" - набор нот в определенном темпе с акцентами.

Не стал сразу отвечать, взял перерыв на подумать - это ты токсик или газлайтишь. Так и не разобрался, кстати :)

  Развернуть 1 комментарий

@ch3sh1r, я тоже удержался от сравнимого по токсичности ответа, что если не испытал "мороз по коже" – твое дело, не мешай другим видеть невероятную красоту в этой истории.

  Развернуть 1 комментарий

это ты токсик или газлайтишь

@ch3sh1r, мне сложно сказать, сам выбери.

Я годы назад читал статью на Хабре об этом чуваке и его подходе к доказательству. В том числе о том, что появились ребята, которые просто решили выделить года своего времени на разбор его труда. Думал тут в конце какой-то эпик будет.

Я, кстати, перечитал, и увидел, что "настоящий фриссон могут почувствовать любители математики", а я даже не любитель. Так что прости, @yorko, "зря быканул"

  Развернуть 1 комментарий

@marat_y, интересно. Каким-то образом проглядел движ с доказательством - в последний раз про abc-гипотезу слышал в универе. Возможно по этому проникся.

  Развернуть 1 комментарий

@marat_y, тут целая россыпь философских вопросов поднимается (можно хотя бы коменты в упомянутой статье на Хабре почитать, если тут кажется скудно), но опровергнуть утверждение "Математик не смог адекватно ответить двум проверяющим, конец истории" тоже сложно :)

  Развернуть 1 комментарий

@yorko, я тоже поймал себя на разочаровании от текста, потому что казалось, что сейчас будет расследование и неожиданные повороты, результаты противоречащие чему-то фундаментальному, а по факту оказалось что статья не о доказательстве гипотезы вовсе, а о доказательствах которые нельзя проверить и о том что иногда математики не хотят объяснять что они там сделали.

Даже за объяснением сути гипотезы нужно переходить по одной из ссылок. Забавная аналогия кстати с обсуждаемым доказательством. Если ожидал увидеть про математику, а оказалось про Мотидзуку, то получается как с кликбейтом и "конец истории".

  Развернуть 1 комментарий

@Darel, сожалею, что не смог достаточно вас развлечь.

  Развернуть 1 комментарий

@Darel, один минус точно признаю - суть гипотезы можно было пересказать, а не отправлять по ссылке.

  Развернуть 1 комментарий

@yorko, на первый раз предупреждение, больше не нарушайте.

  Развернуть 1 комментарий

@Darel, (без иронии) какое правило я нарушил?

Ответ был по сути. Развернутая версия: жизнь - это не сериал, к сожалению, развязки не всегда такие уж захватывающие. На данный момент развязки нет: доказательство есть, в нем нашли косяки, автор что-то токсичное ответил, никто так и не знает, верно ли доказательство. В связи с этим возникает немало философских вопросов. Дальше каждый может сам судить, насколько история захватывающая.

  Развернуть 1 комментарий

Интуитивно кажется что вероятность в одиночку написать > 1000 страниц математических выкладок без ошибок крайне мала, наверное еще сложнее чем аналогичное количество кода без багов. У того-же Уайлса на его 100 страниц доказательства нашли ошибки - при том что у него 7 лет было чтобы это заметить и исправить - думаю тут можно утверждать что доказательство с высокой вероятностью неверное исходя из этой эвристики.
UPD:
Исходя из этой-же эвристики нет нужды вникать в доказательство целиком и инвестировать в него N часов. Нужно просто начать с основ и если автор не непогрешимая машина, довольно скоро мы обнаружим ошибку, скорее всего не дочитав до 50-ой страницы (что и сделали проверяющие).

  Развернуть 1 комментарий

@frenzykryger, со всем согласен. Единственное, Шольце, как я понял, уже с 2012 ковырял доказательство, первое время не особо активно, так как надеялся на коллег из более релевантной области – алгебраической геометрии. Но потом, судя по его замечаниям, он прошелся по всему тексту, даже выражая мнение, что до середины 3-ей части "ничего не происходит", только понятия вводятся. В Corollary 3.12 (которое, несмотря на название "следствие" – ключевойшаг в док-ве) нашел баг, после этого, вероятно, действительно не было смысло читать. Это все отсюда https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/

  Развернуть 1 комментарий

А что фундаментально мешает переложить доказательство на формализованный язык, и пусть компьютер (proof system) проверяет его корректность?

  Развернуть 1 комментарий

@SergeiTikhomirov, но такой машинке на вход ведь надо что-то структурированной подать, не просто исходную статью. Почитайте аннотацию. Кто за нас переведет это все на язык, совместимый с такой системой?

  Развернуть 1 комментарий

@yorko, конечно. Я предполагал, что этим мог бы заняться автор, а кто ещё :)

Можно ли представить будущее математики, где статью на peer-review можно подать только с сопровождающим кодом, который можно будет запихнуть в прувер? Чтобы живые люди оценили high-level, что во всём этом есть какой-то смысл, а компьютер бы подтвердил отсутствие багов.

  Развернуть 1 комментарий

@SergeiTikhomirov, боюсь, тут ограничения как теоретические (теорема Геделя о неполноте) так и практические («вот если бы все» не работает обычно)

  Развернуть 1 комментарий

@SergeiTikhomirov, это можно, но даже high-level трудно оценить. Мне кажется, это примерно как по интерфейсу смарт-контракта (без кода) догадаться, какие у него внутренние инварианты/предусловия/постусловия и как это всё можно заабьюзить.

  Развернуть 1 комментарий

@SergeiTikhomirov, есть еще проблема с автором. Он словил критики даже от бывшего научного руководителя из США из-за того, что мало на контакт идет с пояснениями. А тут требовать от него, чтоб он на язык прувера все переводил…

  Развернуть 1 комментарий

@yorko, а можно по-подробнее, как тут теоремы Гёделя ограничивают автоматическую проверку доказательств а "человеческую" не ограничивают?

  Развернуть 1 комментарий

@cheat_ex, я не делал разграничений между человеческими и автоматическими доказательствами. Теорема Геделя о неполноте ограничивает и те, и те. Комментарий был про то, что мы не достигнем состояния, когда любое доказательство закинем в прувер и тот нам сразу скажет, верно ли доказательство или нет.

  Развернуть 1 комментарий

@cheat_ex, про это (и не только) есть классная книжка: https://en.wikipedia.org/wiki/Godel,_Escher,_Bach

  Развернуть 1 комментарий

@SergeiTikhomirov, Некоторые теоремы доказываются простым перебором. Типа "теорема работает для чисел ДО какого-то очень большого значит работает", но в целом - это все, как используется компьютер.

Чтобы компьютер мог проверить доказательство и ему верили надо:

  1. Чтобы был "компилятор" для языка теорем.
  2. Чтобы в компиляторе не было ошибок
  3. Чтобы в железе не было ошибок.
  Развернуть 1 комментарий

@urtow,

в целом - это все, как используется компьютер

Разве? Я имел в виду системы автоматического доказательства типа Coq. Они основаны не на переборе, а на логических выводах. Подаёшь на вход такие-то объекты с такими-то свойствами, а машина помогает найти цепочку корректных логических переходов от "дано" к "требуется доказать".

Конечно, нужно, чтобы в компиляторе и железе не было ошибок, но разве мы не делаем и так аналогичных предположений про человеческий мозг? Чтобы математик мог проверить доказательство и ему верили, надо, чтобы в его рассуждениях не было ошибок - ну да, хорошо бы :)

P.S. В тему про "работает до какого-то числа" недавно было ролик у 3Blue1Brown, и поначалу там кажется, что вааау, что ж за парадокс, что паттерн держится до N=15, а потом ломается?! Но в видосе объяснено, что никакой там магии нет:

  Развернуть 1 комментарий

@SergeiTikhomirov, итить я залип

  Развернуть 1 комментарий

@zrzst, 3blue1brown – один из факторов, объясняющих мой недосып на длинной дистанции

  Развернуть 1 комментарий

@SergeiTikhomirov, там всё очень, очень, очень плохо, сложно и длинно, мне кажется => без шансов. На курсе "Семантики языков программирования" мы в универе как раз доказывали всякое тривиальное (и не очень) на языке Coq про всякие конструкции языков программирования. Я на первых занятиях думал "в качестве упражнения" доказать формулу для суммы N натуральных чисел, но загнулся где-то в самом начале, когда мне потребовалось скобочки в середине индукционного перехода переставить.

Например, если натуральные числа, то это надо строить аж из аксиом Пеано и теории множеств (или чего-то такого, не шарю подробно). Доказывать ассоциативность для четырёх чисел из трёх, и так далее.

Да даже просто сформулировать утверждение - уже отдельное упражнение.

А ещё в любых статьях и доказательствах пропускается 90% очевидных шагов и допущений, которые нельзя пропускать в формальных доказательствах. Что-нибудь в стиле "для всех попарно различных" или "для всех, кроме очень маленьких, константу точно можно подобрать, оставим как упражнение читателю". Так что это придётся осознать и дописать.

  Развернуть 1 комментарий

@yeputons, то есть мы почти так же далеки от автоматического доказательства рассуждений Мутидзуки, как и от его понимания своим мозгом.

  Развернуть 1 комментарий

@yorko, мне кажется так, да. Да даже с задачей четырёх красок были какие-то тёрки на тему "принимать ли доказательство из тысячи случаев, которые разобрал компьютер".

  Развернуть 1 комментарий

@yeputons, вспоминается статья про активацию SeLU (кажется), где в аппендиксе страниц 60 нечитаемых сгенерированных доказательств. Стало мемом.

  Развернуть 1 комментарий

@yeputons, кажется, что это вопрос привычки — если иметь библиотеку лемм, релевантных для предметной области, и постоянно в этой области в таком ключе работать, то должно быть не слишком сложно (особенно учитывая, что можно поручить бездушной машине перебором искать какой-нибудь несложный переход от одного утверждения к другому). Впрочем, я не особо пытался, разве что ковырял немного PLFA (который хоть и не доковырял, но рекомендую интересующимся).

Вообще огромный разрыв между тем, сколько возможностей предоставляют современные формальные системы, и сложившейся математической культурой (где анекдоты про «потерял лист выкладок — напиши „легко видеть“» оказываются чрезвычайно жизненными) — это совершенно удивительный для меня феномен. Жаль, что попытки с этим что-нибудь сделать (Воеводский с унивалентными основаниями как будто сделал последнюю заметную попытку, и тому довольно ранняя смерть помешала дальше это всё развить — хотя HoTT Book по-прежнему продолжают развивать, но во что-то массовое это не вылилось) случаются редко и не заходят достаточно далеко, чтобы повлиять на статус-кво.

  Развернуть 1 комментарий

@SergeiTikhomirov, я года 3 назад пробовал вкурить автоматические пруверы, в частности Coq. Там всё нереально плохо во-первых с педагогикой, все доступные книжки эталонная херня на тему "оставим в качестве упражнения". Во-вторых, насколько я смог понять, там большие сложности с бибилиотеками и реюзом доказательств. Очень часто одна формулировка теоремы работает для доказательства одних следствий и не работает для доказательства других. На подходе к теореме пифагора я охренел и забил.

  Развернуть 1 комментарий

История Мотидзуки напоминает историю прекрасной женщины из Китая, которая 10 лет переписывала историю России в Википедии, а потом оказалось что она всё это целиком выдумала

  Развернуть 1 комментарий

@iDeBugger, хех, я б не был настолько суров по отношению к Мотидзуки, он все же гений с историей успеха в релевантной области математики и он никого не обманывал. Можно оставить ненулевую плотность вероятности возле такого расклада, что Мотидзуки все доказал, но не справился с тем, чтобы нормально изложить (что, впрочем, ввиду социальности математики как науки означает, что доказательство не валидно).

  Развернуть 1 комментарий

@yorko, о, я видимо упустил что он в, так сказать, конвенциональной математике тоже добился успеха. Тогда вопросов нет!

  Развернуть 1 комментарий

@iDeBugger, да, он в 24 уже получил доктора под руководством филдсовского лауреата. И сам уже уcпел опубликоваться в Annals of Mathematics. Если б это был хрен с горы с док-вом abc-гипотезы, история не была бы настолько захватывающей.

  Развернуть 1 комментарий

А как так на основании того что Мотидзуки вспылил можно сказать, что верность его доказательства очень маловероятна? По-моему исходя из этого можно сказать только что у него софт скилы нулёвые. Даже два других гениальных математика вполне могли запутаться в его доказательстве. Особенно учитывая что все остальные оценивали время необходимое для понимания в год, а они за неделю нашли там недочёт.

Имхо это никакого отношения не имеет к верности/неверности доказательства.

  Развернуть 1 комментарий

@grbit, к самой корректности это отношения не имеет, но имеет к тому, сможет ли научное сообщество подтвердить/опровергнуть эту самую корректность. Если его нулевые софт-скиллы станут блокером для сообщества, то реальная истинность неважна, потому что мы всё равно не сможем использовать неподтвержденную (пусть и корректную) теорию

  Развернуть 1 комментарий

@grbit, я не исключаю, что доказательство может быть технически верным (в посте тоже). Но, как отметил @iDeBugger, это будет иметь только призрачный интерес, поскольку толку от такого доказательства ноль. К слову, Peter Sholtze начал вникать в статьи Мотидзуки очень давно, это только на личную встречу он на неделю прилетел. Больше про подход Sholtze к снаряду написано в этом посте.

  Развернуть 1 комментарий
Maxim Soldatenco учусь и преподаю 28 ноября 2022

Очень живо, но при этом плотно написано, спасибо! Когда читаю о нерешенных проблемах, всегда вспоминаю conjecture Коллаца, то самое о 3x+1.

  Развернуть 1 комментарий

@Uniphot, круто, интересно про 3x+1, формулировка даже проще, чем у abc.

  Развернуть 1 комментарий

😎

Автор поста открыл его для большого интернета, но комментирование и движухи доступны только участникам Клуба

Что вообще здесь происходит?


Войти  или  Вступить в Клуб