когда "Кокуанд, Жояль, Шульман" у тебя PhD принимают :-)

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

если "Жояль", тогда уже и "Кокан"

Я согласен на всё!

так Симпсон нашел или Воеводский? :)

Симпсон помог Воеводскому, контрибютор

Симпсон постоил контрпример к одной из фундаментальных для доказательства лемм. Воеводский искал ошибку в доказательстве этой леммы. Потом в построении контрпримера Симпсона. Потом снова в своём доказательстве. В процессе по своим признаниям чуть не съехал крышей и даже успел усомниться в непротиворечивости арифметики.

А потом таки нашёл ошибку в своём доказательстве.

Вот это история!

И соответственно пришлось всё переколбасить и подрихтовать результат, он оказался несколько слабее.

Вот Ален Конн тоже является умеренным сторонником формальной верификации из-за трудного опыта.

Я уже точно не помню год, но было это в районе 2006-2007. Ален Конн тогда наконец доказал теоремму о реконструкции, венец и маковку фундамента своей некоммутативной дифференциальной геометрии: теорему о том, что из спектральной тройки, построенной из риманового- или спин-многообразия можно получить многообразие назад (это тройка состоит из гильбертова пространства квадратично-интегрируемых распределения на многообразии, действующей на нём линейно C*-алгебре гладких функций на этом многообразии, и действующего на нём же согласованно с гладкими функциями оператора Дирака, играющего роль обобщённой римановой метрики.)

Теорема эта весьма монументальна. Её доказательство занимает, если я не ошибаюсь, 193 страницы, и мы разбирали его на семинаре весь семестр.

Исправно по главе доказательства за семинар, но на некоторые таки уходило два.

тут даже из учебника ХоТТ не получается перенести на cubical, что и говорить про такие глобальные работы, это же целые специализированые библиотеки.

гладкие функции на многообразии же не образуют С*

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

Гладкие комплекснозначные функции на компактном многообразии — образуют. А если оно некомпактное, то делу можно помочь, если оно хотя бы локально-компактное: следует взять алгебру быстро зануляющихся гладких комплекснозначных функций.

Эта алгебра будет неунитальна, но тем не менее всё работает с некоторыми небольшими усложнениями.

Какая там норма?