Прорыв в функциональном анализе в начале пятидесятых связан с работами Сергея Львовича Соболева и Лорана Шварца (маленький исторический обзор). Они исследовали пространства обобщённых функций, распределений, и доказали мощные теоремы о существовании решений PDE, которыми математики пользуются по сей день.
На другом конце света Микио Сато (интервью), вдохновлённый школой Гротендика, которая как раз в это время производила революцию в алгебраической геометрии, решил, что бесконечномерные банаховы пространства распределений не отвечают духу времени. Сато создавал алгебраическую теорию обобщённых функций, которые он назвал гиперфункциями.
Киотская школа: Сато, его ученики Масаки Кашивара, Такахиро Кавай, позднее Тэцудзи Мива, Мичио Джимбо развили теорию гиперфункций, которая со временем переросла в микролокальный анализ и, с помощью Пьера Шапира, в микролокальную теорию пучков, см. очень хороший недавний обзор (Шапира, 2017).
Сегодня микролокальный взгляд на конструктивные пучки в сущности стал общим знанием. Он проник и прижился в теории PDE, симплектической топологии, зеркальной симметрии и смежных областях.
На этот текст меня вдохновил чудесный доклад Roger Casals о его открытии важности микролокальной теории для изучения лагранжевых узлов. Они обнаружили, что на стеке модулей конструктивных пучков на плоскости с микролокальным носителем на данном лежандровом узле есть структура кластерного многообразия, что позволяет строить бесконечно много лагранжевых заполнений узла с помощью кластерных мутаций. Доклад абсолютно прекрасный и довольно элементарный.
На другом конце света Микио Сато (интервью), вдохновлённый школой Гротендика, которая как раз в это время производила революцию в алгебраической геометрии, решил, что бесконечномерные банаховы пространства распределений не отвечают духу времени. Сато создавал алгебраическую теорию обобщённых функций, которые он назвал гиперфункциями.
Киотская школа: Сато, его ученики Масаки Кашивара, Такахиро Кавай, позднее Тэцудзи Мива, Мичио Джимбо развили теорию гиперфункций, которая со временем переросла в микролокальный анализ и, с помощью Пьера Шапира, в микролокальную теорию пучков, см. очень хороший недавний обзор (Шапира, 2017).
Сегодня микролокальный взгляд на конструктивные пучки в сущности стал общим знанием. Он проник и прижился в теории PDE, симплектической топологии, зеркальной симметрии и смежных областях.
На этот текст меня вдохновил чудесный доклад Roger Casals о его открытии важности микролокальной теории для изучения лагранжевых узлов. Они обнаружили, что на стеке модулей конструктивных пучков на плоскости с микролокальным носителем на данном лежандровом узле есть структура кластерного многообразия, что позволяет строить бесконечно много лагранжевых заполнений узла с помощью кластерных мутаций. Доклад абсолютно прекрасный и довольно элементарный.
arXiv.org
Sobolev and Schwartz: Two Fates and Two Fames
This is a brief overview of the lives and contributions of S.L. Sobolev and L. Schwartz, the cofounders of distribution theory.
#классно
Прошло полтора месяца. Новая нейросеть о3 научилась подбирать ответ к каждой четвёртой задаче очень сложного и математически содержательного бенчмарка Frontier Math, который мы обсуждали выше. Раньше лучшие нейронки выдавали всего два процента.
Здорово. Чем быстрее компьютеры станут полезными для настоящих исследовательских задач, тем быстрее мы сможем их применять в рисёрче.
Прошло полтора месяца. Новая нейросеть о3 научилась подбирать ответ к каждой четвёртой задаче очень сложного и математически содержательного бенчмарка Frontier Math, который мы обсуждали выше. Раньше лучшие нейронки выдавали всего два процента.
Здорово. Чем быстрее компьютеры станут полезными для настоящих исследовательских задач, тем быстрее мы сможем их применять в рисёрче.
#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.
В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.
Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.
Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.
Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.
Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------
Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.
Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.
В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.
Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.
Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.
Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.
Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------
Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.
Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!
Xena
Beyond the Liquid Tensor Experiment
The liquid tensor experiment is now fully completed.
Veni, Deus ex machina!
-----
• ИИ индустрия будет расти и развиваться. Чего только стоит недавний проект Stargate, по которому Штаты за пять лет потратят полтриллиона долларов на строительство датацентров для тренировки моделей. В это время желающие: французы из Mistral, китайцы из DeepSeek, или сберовцы с GigaСhat, могут гнаться за прогрессом, обучая свои модели быть умнее, быстрее, дешевле.
• Современные модели уже прошли большинство тестов а-ля Тьюринг, считавшиеся раньше непреодолимыми. Сегодняшние бенчмарки -- либо чистая сложная математика, как FrontierMath, либо на >40% очень сложная математика, как недавний Humanity's Last Exam (посмотрите, задачи совершенно фантастические. Особенно про Ясона).
• В стремлении создать лучшую модель, компании будут обучаться на математические бенчмарки. Математики с радостью идут к ним навстречу: скажем, Тао недавно взялся распределять девять миллионов долларов на развитие связки Lean+LLM для автоматического доказательства теорем.
• В момент, когда нейронки научатся стабильно решать большую часть задач из FrontierMath математика как наука изменится так же, как изменилась работа шахтёров после изобретения динамита и бурильных машин. И тогда мы...
Мы станем операторами систем ИИ, решим открытые гипотезы, которые и не надеялись решить, по-новому поймём математику, переизобретём матфизику, биоинформатику, квантовую химию, соберём разрозненные уголки математического лабиринта в мощный единый аппарат познания окружающего мира и познания самих себя.
Наступит следующий виток эволюции науки. Future shining bright 🌄
-----
• ИИ индустрия будет расти и развиваться. Чего только стоит недавний проект Stargate, по которому Штаты за пять лет потратят полтриллиона долларов на строительство датацентров для тренировки моделей. В это время желающие: французы из Mistral, китайцы из DeepSeek, или сберовцы с GigaСhat, могут гнаться за прогрессом, обучая свои модели быть умнее, быстрее, дешевле.
• Современные модели уже прошли большинство тестов а-ля Тьюринг, считавшиеся раньше непреодолимыми. Сегодняшние бенчмарки -- либо чистая сложная математика, как FrontierMath, либо на >40% очень сложная математика, как недавний Humanity's Last Exam (посмотрите, задачи совершенно фантастические. Особенно про Ясона).
• В стремлении создать лучшую модель, компании будут обучаться на математические бенчмарки. Математики с радостью идут к ним навстречу: скажем, Тао недавно взялся распределять девять миллионов долларов на развитие связки Lean+LLM для автоматического доказательства теорем.
• В момент, когда нейронки научатся стабильно решать большую часть задач из FrontierMath математика как наука изменится так же, как изменилась работа шахтёров после изобретения динамита и бурильных машин. И тогда мы...
Мы станем операторами систем ИИ, решим открытые гипотезы, которые и не надеялись решить, по-новому поймём математику, переизобретём матфизику, биоинформатику, квантовую химию, соберём разрозненные уголки математического лабиринта в мощный единый аппарат познания окружающего мира и познания самих себя.
Наступит следующий виток эволюции науки. Future shining bright 🌄
В честь позавчерашней статьи DeepMind об AlphaGeometry2 (обзор) вот те две геомы: 2018.6 и 2023.6, которые она не смогла решить. Красивые.
Делаем ставки: успеют ли люди записать решения все задач IMO в Lean вручную раньше, чем дипмайнды зарелизят AlphaProof и AlphaGeometry, которые сделают это автоматически.
Делаем ставки: успеют ли люди записать решения все задач IMO в Lean вручную раньше, чем дипмайнды зарелизят AlphaProof и AlphaGeometry, которые сделают это автоматически.
This media is not supported in your browser
VIEW IN TELEGRAM
Множества Мультиброта получаются если в определении множества Мандельброта заменить 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.
-------
Вы помните, в прошлом году 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.
goedel-lm.github.io
Goedel-Prover
Pushing the Limit of Automated Theorem Proving Through Large Scale Data Synthesizing