#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.

Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.

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

Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

Новогодние шапки для ваших записок и статей 🎅🤶

С наступающим Новым годом! Пусть математика будет прекрасным миром открытий и озарений для всех нас в будущем году. Читайте, пишите, любите и творите!

Многие играли в настольную игру SET.

Дана колода из 81 карты, у каждой по четыре признака: цвет, форма, количество, заливка. Set'ом называется три карты, которые по каждому из признаков либо одинаковы, либо попарно различны. Карты выкладываются на стол, и игроки на скорость ищут и собирают set'ы.

Возникает естественный вопрос: сколько бывает карт среди которых нет ни одного сета?

Обычно играют на 12 картах, но частенько сетов не находится, и нужно бывает увеличить до 15 и даже 18 карт. А однажды в игре мне мне пришлось поднять до 19 карт. Всегда ли этого достаточно?

Ответ: нет. На картинке 20 карт без сета!

Это максимум; по ссылке Ben Davis and Diane Maclagan объясняют, что среди 21 карты всегда есть сет, и изучают более многомерные версии SET'а.

-----------

Позабавило их предложение играть в SET из 243 карт тремя обычными колодами с разными запахами

we can play a five-attribute version of set by using scratch-and-sniff set cards with three different odors.

Veni, Deus ex machina!
-----

• ИИ индустрия будет расти и развиваться. Чего только стоит недавний проект Stargate, по которому Штаты за пять лет потратят полтриллиона долларов на строительство датацентров для тренировки моделей. В это время желающие: французы из Mistral, китайцы из DeepSeek, или сберовцы с GigaСhat, могут гнаться за прогрессом, обучая свои модели быть умнее, быстрее, дешевле.

• Современные модели уже прошли большинство тестов а-ля Тьюринг, считавшиеся раньше непреодолимыми. Сегодняшние бенчмарки -- либо чистая сложная математика, как FrontierMath, либо на >40% очень сложная математика, как недавний Humanity's Last Exam (посмотрите, задачи совершенно фантастические. Особенно про Ясона).

• В стремлении создать лучшую модель, компании будут обучаться на математические бенчмарки. Математики с радостью идут к ним навстречу: скажем, Тао недавно взялся распределять девять миллионов долларов на развитие связки Lean+LLM для автоматического доказательства теорем.

• В момент, когда нейронки научатся стабильно решать большую часть задач из FrontierMath математика как наука изменится так же, как изменилась работа шахтёров после изобретения динамита и бурильных машин. И тогда мы...

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

Наступит следующий виток эволюции науки. Future shining bright 🌄

#цитата
Читаю книжку. Понравилось начало секции Uncontents:

As unbirthdays sometimes provide with more gifts and excitement than birthdays,
the “uncontents” of these notes probably constitute the most interesting part of
the topic, and it is worth mentioning the aspects that will not be evocated along
these lines <...>

Прошлогоднее интервью Терри Тао о будущем математики. Он видит прогресс нейросетей как шаг в сторону индустриализации математики, постановки теорем на поток:

I think in three years AI will become useful for mathematicians. It will be a great co-pilot. You’re trying to prove a theorem, and there’s one step that you think is true, but you can’t quite see how it’s true. And you can say, “AI, can you do this stuff for me?” And it may say, “I think I can prove this.” I don’t think mathematics will become solved. If there was another major breakthrough in AI, it’s possible, but I would say that in three years you will see notable progress, and it will become more and more manageable to actually use AI. And even if AI can do the type of mathematics we do now, it means that we will just move to a to a higher type of mathematics. So right now, for example, we prove things one at a time. It’s like individual craftsmen making a wooden doll or something. You take one doll and you very carefully paint everything, and so forth, and then you take another one. The way we do mathematics hasn’t changed that much. But in every other type of discipline, we have mass production. And so with AI, we can start proving hundreds of theorems or thousands of theorems at a time. And human mathematicians will direct the AIs to do various things. So I think the way we do mathematics will change, but their time frame is maybe a little bit aggressive.

<...>

I think there’ll be different ways of doing mathematics that just don’t exist right now. I can see project manager mathematicians who can organize very complicated projects—they don’t understand all the mathematics, but they can break things up into smaller pieces and delegate them to other people, and they have good people skills. Then there are specialists who work in subfields. There are people who are good at trying to train AI on specific types of mathematics, and then there are people who can convert the AI proofs into something human-readable. It will become much more like the way almost any other modern industry works. Like, in journalism, not everyone has the same set of skills. You have editors, you have journalists, and you have businesspeople, and so forth—we’ll have similar things in mathematics eventually.

По опыту, ждать три года не нужно, разговаривать с дипсиком и чатгпт о математике можно уже сейчас. Они уже довольно неплохо считают. И знакомиться с новой областью теперь можно в стиле Хэмингуэя :)

Я расскажу тебе о теории КАМ. Чётко, ясно, как диагональная матрица.

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

Так думали. Так говорил Пуанкаре. Он смотрел на задачу трёх тел и видел хаос. Лиувилльская теорема больше не спасала, интегралы движения исчезали, а с ними — и регулярные орбиты.

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

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

Мозер довёл дело до конца. Его нормальные формы позволили описать процесс устойчивости и разрушения торов, уточнив границы применимости теории.

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

Это теория о том, как гармония сопротивляется хаосу. Как порядок ускользает, но не исчезает. Как динамика сложна, но не всегда непредсказуема. Как среди бури остаются тихие гавани, где движение продолжается вечно.



Множества Мультиброта получаются если в определении множества Мандельброта заменить z -> z^2 + c на z -> z^d + c для какого-то d. Мы с дипсиком сделали анимацию для дробных d. Получаются смешные фрактальные сердечки

А у ВольфрамАльфа можно научиться принимать комплименты

Вышли две новые опенсорсные LLM-ки для автоматического доказательства теорем.

-------
Вы помните, в прошлом году DeepMind делали заголовки AlphaProof'ом, который, как утверждалось, решил четыре задачи с последнего межнара, чего хватило бы на серебро. Но исходного кода нам не показали, лишь файлы со сгенерированными Lean-решениями этих четырёх задач.

Чуть позже DeepSeek выложили в опенсорс свою небольшую бям DeepSeek-Prover-V1.5 на 7B. Они реализовали версию метода Монте-Карло поиска по дереву всевозможных доказательств, как в шахматных движках. Модель занимается генерацией доказательства в Lean, а когда оно перестаёт компилироваться, она обрезает до первой ошибки и пробует с разными тактиками доказать промежуточные утверждения, которые приблизят её к цели. И поверх ещё обучение с подкреплением.

Главная проблема — в ограниченности обучающей выборки. Не так много кода люди написали в Lean; самый большой его источник — библиотека Mathlib.

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

-------
На этой неделе вышел Goedel-Prover, где авторы реализовали эту идею. Они начали с DeepSeek-Prover-V1.5 и построили цепочку из десяти моделей, последовательно генерирующих больше и больше верных доказательств. Последняя модель оказалась довольно сильной и выбила SOTA.

Другая недавняя статья предлагает Self-play Theorem Prover. Авторы берут тот же DeepSeek-Prover-V1.5 и делят его на conjecturer и prover. Идея в том, чтобы conjecturer переформулировал исходное утверждение, придумывал разные связанные гипотезы, а prover их доказывал. Они придумали интересный процесс обучения, чтобы заставить conjecturer изобретать нетривиальные, но и не совсем уж сложные гипотезы, которые действительно помогут в доказательстве. Они тоже выбивают SOTA (честно пишут, что восемь раз обучились на валидации).

Пруверы оценивают на трёх бенчмарках: школьные задачи (сейчас SOTA ~60%), университетские задачи — матан, линал, общая топология — сейчас SOTA 25%, и задачи с Putnam — олимпиада среди университетов — сейчас SOTA восемь задач (всего 664).

Забавная деталь о методологии: к каждой задаче генерируется несколько возможных решений, которые затем проверяются Lean'ом, и если нашлось подходящее — задача считается решённой. Например, 60% выше получаются, если разрешить DeepSeek-Prover-V1.5 генерировать по 102400 (сто тысяч) решений на задачу. А если только по 128, получается ~50%.

-----
Такие вот дела. И все эти модели маленькие, помещаются на одну домашнюю видеокарту. Можно запускать локально. Если теперь вставить туда по-настоящему большие модели, как Orion или грядущий GPT-5 со встроенным reasoning'ом могут получиться результаты поинтереснее. А пока чистая GPT-4o гордо решает ровно 1 (одну) задачу с Putnam.

Воспоминания Пауло Рибенбойма об Александре Гротендике, они дружили.

Пауло рассказывает:
• друзья звали Гротендика Шуриком;
• о бразильском периоде;

• “My theories are like enormous trees from which the theorems fall like ripe fruits.”;

• Пауло убеждён, что Шурик ни одной книги не прочёл от корки до корки;
• Шурик не поехал в Москву на вручении премии Филдса в 1966 году потому что был против преследования Даниеля и Синявского;
• Шурик занимался только наукой, у которой не было даже теоретического военного применения;
• Шурик брился налысо и ходил в чёрном, подражая стилистике русского muzhik;
• у Шурика не было французского гражданства. На его заднем дворе регулярно обретались диссиденты и буддийские монахи;
• о борьбе за экологию;
• о поздних годах.

Пауло почти не рассказывает о математике Гротендика, но о ней, например, писал Пьер Картье. Там же он размышляет об отце, Александре Шапиро, его борьбе против царизма, о мировоззрении Гротендика и его наследии.
Ещё есть воспоминания Юрия Манина о Гротендике и генезисе теории мотивов.

Ну и конечно книга Урожаи и посевы, которую можно целиком разбирать на цитаты.

Терри Тао считает что социально приемлимо во время доклада вне своей области экспертизы параллельно расспрашивать нейросеть. Он поделился логом своего разговора с ChatGPT во время доклада о программе Ленглендса и когомологиях многообразий Шимуры: https://chatgpt.com/share/67c0be9e-17cc-800e-a222-c4328287d619

Тао пишет что для целей математики

any modern model would give satisfactory results for any topic that has a non-trivial Wikipedia page.

Имхо, в процессе вхождения в новую область знания обсуждение её с нейронкой практически обязательно. Она и статьи найдёт, и интуицию кое-какую объяснит, и примеры подберёт, и вычисления сделает, и картинку нарисует. Очень упрощает рутину, как автопилот в самолёте. Или как трудолюбивый домовой эльф.

Round About Four Dimensions
Aluminium, stainless steel, brass, polymers, electronics; 230 x 230 x 230 cm
Julius von Bismarck & Benjamin Maus, CERN, Switzerland, 2023

↑ Понравился двухметровый роботизированный тессеракт из ЦЕРНа. Пришлось сделать вебстраничку с вращающимся тессерактом чтобы вдоволь поиграться.

Масаки Кашивара получил премию Абеля! За алгебраический анализ (писал о нём выше) и вклад в теорию представлений (хотя на мой взгляд Джордж Люстиг сделал не меньше). Пьер Шапира рассказывал о математике Кашивары на конгрессе в 2018: тык

Поздравляем! Кашивара один из самых моих любимых математиков 🥰