От исходного кода до процессора: разберись, как работает программа 💻
Стартует практический курс YADRO «Системное программирование с использованием языка С» для тех, кто уже знаком с синтаксисом C и хочет разобраться, как программа работает изнутри.
Формат: курс пройдет онлайн с октября 2026 по май 2027 года. Занятия — раз в неделю, где 80% времени будет посвящено практике.
Этот курс для тебя, если ты:
🔵 учишься в вузе;
🔵 уверенно владеешь базовыми конструкциями C;
🔵 понимаешь, как работают указатели, структуры данных и динамическая память;
🔵 знаешь основные алгоритмы и структуры данных.
*️⃣ Будет плюсом опыт разработки под Linux.
Материалы для подготовки и форму регистрации можно найти — по ссылке 🔗
Стартует практический курс YADRO «Системное программирование с использованием языка С» для тех, кто уже знаком с синтаксисом C и хочет разобраться, как программа работает изнутри.
Формат: курс пройдет онлайн с октября 2026 по май 2027 года. Занятия — раз в неделю, где 80% времени будет посвящено практике.
Этот курс для тебя, если ты:
🔵 учишься в вузе;
🔵 уверенно владеешь базовыми конструкциями C;
🔵 понимаешь, как работают указатели, структуры данных и динамическая память;
🔵 знаешь основные алгоритмы и структуры данных.
*️⃣ Будет плюсом опыт разработки под Linux.
Материалы для подготовки и форму регистрации можно найти — по ссылке 🔗
18 сентября — приходи на онлайн-трансляцию, где мы расскажем подробнее о практических курсах и ответим на все вопросы. После вебинара пройдет обзорная лекция про системное программирование и роль языка С. Регистрация — здесь.
❤3👍2
Forwarded from Математическая свалка Сепы (Sergei)
ИИ помог формализовать доказательство Перельмана
Команда математиков сообщила о полной формализации доказательства гипотезы Пуанкаре на языке Lean — при помощи ИИ.
Результат, полученный Григорием Перельманом в 2002–2003 годах, перевели в форму, позволяющую компьютеру проверять каждый логический шаг.
За проектом стоит межвузовская команда из США:
Bennett Chow (University of California San Diego)
Yuan Liao (University of California San Diego)
Ziyang Qin (Cornell University, Math+AI Lab)
Ayush Khaitan (Princeton University, Princeton Language and Intelligence)
Общая тема этой коллаборации — геометрия и автоматизация математических доказательств. Они создают библиотеку, в которой результаты современной математики доступны для машинной проверки и дальнейшего использования.
Математики определяли стратегию и проверяли формулировки, ИИ помогал писать формальные доказательства, а Lean проверял их логическую корректность.
Код открыт; авторы заявляют отсутствие пропущенных доказательств. Автоматическая сборка проекта прошла успешно.
🔗 Код и описание проекта · Результат автоматической проверки
Команда математиков сообщила о полной формализации доказательства гипотезы Пуанкаре на языке Lean — при помощи ИИ.
Результат, полученный Григорием Перельманом в 2002–2003 годах, перевели в форму, позволяющую компьютеру проверять каждый логический шаг.
За проектом стоит межвузовская команда из США:
Bennett Chow (University of California San Diego)
Yuan Liao (University of California San Diego)
Ziyang Qin (Cornell University, Math+AI Lab)
Ayush Khaitan (Princeton University, Princeton Language and Intelligence)
Общая тема этой коллаборации — геометрия и автоматизация математических доказательств. Они создают библиотеку, в которой результаты современной математики доступны для машинной проверки и дальнейшего использования.
Математики определяли стратегию и проверяли формулировки, ИИ помогал писать формальные доказательства, а Lean проверял их логическую корректность.
Код открыт; авторы заявляют отсутствие пропущенных доказательств. Автоматическая сборка проекта прошла успешно.
🔗 Код и описание проекта · Результат автоматической проверки
🔥14🤣3💘1
«Book of Proof» Ричарда Хэммака помогает учиться читать, понимать и строить математические доказательства. Учебник полностью бесплатный и особенно подходит студентам первых курсов, осваивающим строгие математические рассуждения.
На почти 400 страницах разбираются теория множеств, логика и комбинаторика, прямые доказательства, методы контрапозиции и от противного, математическая индукция. В содержание также входят отношения, функции, доказательства в математическом анализе и мощности множеств. В книге много упражнений и решений.
PDF книги
https://richardhammack.github.io/BookOfProof/Main.pdf
На почти 400 страницах разбираются теория множеств, логика и комбинаторика, прямые доказательства, методы контрапозиции и от противного, математическая индукция. В содержание также входят отношения, функции, доказательства в математическом анализе и мощности множеств. В книге много упражнений и решений.
PDF книги
https://richardhammack.github.io/BookOfProof/Main.pdf
1👍10🔥4✍2
Теорема о четырёх красках гарантирует, что любой планарный граф без петель можно раскрасить в четыре цвета. В работе 2026 года «The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring» авторы предлагают новое доказательство и алгоритм раскраски за O(n log n), где n обозначает число вершин. Предыдущий алгоритм, с которым они сравнивают результат, требовал квадратичного времени.
Главная перемена касается того, насколько сильно удаётся уменьшить граф за один этап. В прежних доказательствах находили подходящую для редукции конфигурацию или специальный цикл, уменьшали граф на постоянное число вершин и переходили к меньшей задаче. Один такой шаг занимал линейное время, а вся процедура давала квадратичную оценку.
В новой работе авторы доказывают, что каждая планарная триангуляция содержит линейное по числу вершин количество попарно не соприкасающихся редуцируемых конфигураций либо попарно не пересекающихся препятствующих циклов длины не более пяти. Оба типа структур позволяют выполнять редукции при построении четырёхцветной раскраски. Благодаря этому размер задачи удаётся уменьшать в постоянное число раз за этап.
Важная часть результата связана с большими «плоскими» участками графа. Прежние доказательства находили нужные конфигурации там, где локальная комбинаторная кривизна положительна. Авторы показывают, что подходящие редукции существуют и на больших участках с нулевой кривизной.
При этом компьютерная часть доказательства стала масштабнее. Авторы используют более 8200 D-редуцируемых конфигураций и проверяют конечные наборы случаев программами на C++. Они отдельно оговаривают, что их доказательство не является формальным доказательством в смысле работы Гонтье. Ускорение алгоритма раскраски здесь сочетается с большим объёмом компьютерных проверок самого доказательства.
Ссылка - https://arxiv.org/abs/2603.24880
История задачи и рассказ о новом результате в Quanta Magazine.
https://www.quantamagazine.org/the-four-color-theorem-gets-a-rare-new-proof-20260910/
Главная перемена касается того, насколько сильно удаётся уменьшить граф за один этап. В прежних доказательствах находили подходящую для редукции конфигурацию или специальный цикл, уменьшали граф на постоянное число вершин и переходили к меньшей задаче. Один такой шаг занимал линейное время, а вся процедура давала квадратичную оценку.
В новой работе авторы доказывают, что каждая планарная триангуляция содержит линейное по числу вершин количество попарно не соприкасающихся редуцируемых конфигураций либо попарно не пересекающихся препятствующих циклов длины не более пяти. Оба типа структур позволяют выполнять редукции при построении четырёхцветной раскраски. Благодаря этому размер задачи удаётся уменьшать в постоянное число раз за этап.
Важная часть результата связана с большими «плоскими» участками графа. Прежние доказательства находили нужные конфигурации там, где локальная комбинаторная кривизна положительна. Авторы показывают, что подходящие редукции существуют и на больших участках с нулевой кривизной.
При этом компьютерная часть доказательства стала масштабнее. Авторы используют более 8200 D-редуцируемых конфигураций и проверяют конечные наборы случаев программами на C++. Они отдельно оговаривают, что их доказательство не является формальным доказательством в смысле работы Гонтье. Ускорение алгоритма раскраски здесь сочетается с большим объёмом компьютерных проверок самого доказательства.
Ссылка - https://arxiv.org/abs/2603.24880
История задачи и рассказ о новом результате в Quanta Magazine.
https://www.quantamagazine.org/the-four-color-theorem-gets-a-rare-new-proof-20260910/
arXiv.org
The Four Color Theorem with Linearly Many Reducible Configurations...
We give a near-linear time 4-coloring algorithm for planar graphs, improving on the previous quadratic time algorithm by Robertson et al. from 1996. Such an algorithm cannot be achieved by the...
🔥9👍2
6 октября 2026 года OpenAI объявила о публикации математических результатов, полученных внутренней ИИ-моделью. По сообщению компании, результаты размещены в GitHub-репозитории с правилами внесения исправлений в рукописи и цитирования.
Для многих доказательств опубликованы формализации на Lean, языке программирования, который позволяет проверять математические доказательства на компьютере. OpenAI обещает добавлять новые формализации по мере их получения. В сообщении речь идёт о многих доказательствах, а не о формальной проверке всей коллекции.
Компания также сообщает о публикации десяти кратких изложений рассуждений модели, оценок вычислительных затрат и статистики числа задач, которые она пыталась решить. Средние затраты на один результат OpenAI оценивает как эквивалент примерно трёх часов работы ChatGPT Pro в режиме размышления.
Объявление OpenAI
https://openai.com/index/sharing-ai-progress-in-mathematics/
Файл overview.pdf в репозитории
https://github.com/openai/math/blob/main/overview.pdf
Наш канал в MAX
https://max.ru/mathematic
#Математика #Статистика #МатематическоеМоделирование #Доказательства
Для многих доказательств опубликованы формализации на Lean, языке программирования, который позволяет проверять математические доказательства на компьютере. OpenAI обещает добавлять новые формализации по мере их получения. В сообщении речь идёт о многих доказательствах, а не о формальной проверке всей коллекции.
Компания также сообщает о публикации десяти кратких изложений рассуждений модели, оценок вычислительных затрат и статистики числа задач, которые она пыталась решить. Средние затраты на один результат OpenAI оценивает как эквивалент примерно трёх часов работы ChatGPT Pro в режиме размышления.
Объявление OpenAI
https://openai.com/index/sharing-ai-progress-in-mathematics/
Файл overview.pdf в репозитории
https://github.com/openai/math/blob/main/overview.pdf
Наш канал в MAX
https://max.ru/mathematic
#Математика #Статистика #МатематическоеМоделирование #Доказательства
🔥1
13 ноября 2026 года оказалось датой «конца света» в демографическом прогнозе, опубликованном в Science ещё в 1960 году. Хайнц фон Фёрстер, Патриция Мора и Лоуренс Амиот экстраполировали рост населения и получили приближение его численности к бесконечности в конечный момент времени.
За эффектной датой стояла гипотеза о человеческой кооперации. Чем больше людей, тем больше возможностей общаться, объединяться и совместно решать проблемы. Авторы предположили, что такая обратная связь способна поддерживать рост быстрее экспоненциального. Для сопоставления с историей они использовали 24 оценки численности населения за две тысячи лет.
Здесь важна оговорка. Приближение к бесконечности было результатом продолжения выбранной модели в будущее. Само предположение о росте быстрее экспоненциального ещё не означает, что бесконечность будет достигнута за конечное время.
Прогноз некоторое время оставался удачным. В 1970-х и 1980-х годах уравнение давало оценки точнее прогнозов многих демографов. Примерно с 1993 года население мира стало отставать от предсказанной траектории.
Этот сюжет помогает разделить два вопроса о математической модели. Насколько хорошо она описывает наблюдения? И насколько далеко в будущее можно продолжать её закономерность? Даже удачное совпадение с данными на протяжении десятилетий не гарантирует, что режим роста сохранится вплоть до предсказанной сингулярности.
Наш канал в MAX
https://max.ru/mathematic
#Моделирование #Демография #ИсторияМатематики #Прогнозы
За эффектной датой стояла гипотеза о человеческой кооперации. Чем больше людей, тем больше возможностей общаться, объединяться и совместно решать проблемы. Авторы предположили, что такая обратная связь способна поддерживать рост быстрее экспоненциального. Для сопоставления с историей они использовали 24 оценки численности населения за две тысячи лет.
Здесь важна оговорка. Приближение к бесконечности было результатом продолжения выбранной модели в будущее. Само предположение о росте быстрее экспоненциального ещё не означает, что бесконечность будет достигнута за конечное время.
Прогноз некоторое время оставался удачным. В 1970-х и 1980-х годах уравнение давало оценки точнее прогнозов многих демографов. Примерно с 1993 года население мира стало отставать от предсказанной траектории.
Этот сюжет помогает разделить два вопроса о математической модели. Насколько хорошо она описывает наблюдения? И насколько далеко в будущее можно продолжать её закономерность? Даже удачное совпадение с данными на протяжении десятилетий не гарантирует, что режим роста сохранится вплоть до предсказанной сингулярности.
Наш канал в MAX
https://max.ru/mathematic
#Моделирование #Демография #ИсторияМатематики #Прогнозы
❤3👍1
Как оценивать работу математика, если ИИ всё активнее участвует в получении результатов?
Павел Этингоф и Слава Герович обсуждают этот вопрос в эссе Mathematics of the Future.
Авторы предполагают, что развитие ИИ изменит устройство математической профессии. Они предлагают уменьшить акцент на приоритете и списке публикаций, придавая больше значения глубокому пониманию, самостоятельности суждений, выбору направлений исследования и умению объяснять математику.
В этой картине работа с ИИ включает несколько содержательных задач. Математики могут исследовать расширяющийся круг результатов, интерпретировать и связывать знания, полученные с помощью ИИ, исправлять и формализовать существующую литературу, разрабатывать новые формы изложения и публикации.
Из этого вытекает и предложение об оценке исследователей. При найме и в подготовке аспирантов Этингоф и Герович предлагают больше опираться на длительное математическое взаимодействие. Доклады, обсуждения, устные экзамены, наставничество и совместная работа должны играть более заметную роль, а статьи не должны служить единственным решающим свидетельством способностей.
Для исследовательских групп авторы намечают модель, сочетающую коллективное человеческое размышление с осторожным использованием и проверкой ответов ИИ. При этом они признают серьёзные этические, социальные и связанные с надёжностью знания проблемы и подчёркивают уважение к тем, кто решает обходиться без ИИ.
Центральной целью такого переустройства они считают сохранение и расширение человеческой способности развивать, понимать и передавать математику.
Наш канал в MAX
https://max.ru/mathematic
#математика #искусственныйинтеллект #исследования #матобразование
Павел Этингоф и Слава Герович обсуждают этот вопрос в эссе Mathematics of the Future.
Авторы предполагают, что развитие ИИ изменит устройство математической профессии. Они предлагают уменьшить акцент на приоритете и списке публикаций, придавая больше значения глубокому пониманию, самостоятельности суждений, выбору направлений исследования и умению объяснять математику.
В этой картине работа с ИИ включает несколько содержательных задач. Математики могут исследовать расширяющийся круг результатов, интерпретировать и связывать знания, полученные с помощью ИИ, исправлять и формализовать существующую литературу, разрабатывать новые формы изложения и публикации.
Из этого вытекает и предложение об оценке исследователей. При найме и в подготовке аспирантов Этингоф и Герович предлагают больше опираться на длительное математическое взаимодействие. Доклады, обсуждения, устные экзамены, наставничество и совместная работа должны играть более заметную роль, а статьи не должны служить единственным решающим свидетельством способностей.
Для исследовательских групп авторы намечают модель, сочетающую коллективное человеческое размышление с осторожным использованием и проверкой ответов ИИ. При этом они признают серьёзные этические, социальные и связанные с надёжностью знания проблемы и подчёркивают уважение к тем, кто решает обходиться без ИИ.
Центральной целью такого переустройства они считают сохранение и расширение человеческой способности развивать, понимать и передавать математику.
Наш канал в MAX
https://max.ru/mathematic
#математика #искусственныйинтеллект #исследования #матобразование
👍3👏1
SAIR Open Math OS запущена в ранней версии. Платформа предоставляет веб-интерфейсы для работы с открытыми ИИ-моделями над математическими задачами. Сейчас на ней размещены DeepSeek V4.1 Flash, Kimi K3 и GLM 5.3 Flash.
По оценке команды проекта, эти модели примерно на год отстают от передовых по возможностям. От них не стоит ожидать решения сложных задач с одной попытки. Среди более реалистичных применений команда называет формализацию умеренного объёма в Lean, краткое изложение математических рассуждений и обсуждение математических тем.
Особенность платформы состоит в акценте на командных аккаунтах. Участники одной команды видят запросы друг друга. Разработчики предполагают, что такой формат может быть полезен для совместных проектов.
Вычислительные ресурсы предоставлены проекту в качестве пожертвований. Команда начала выдавать бесплатные аккаунты заявителям из академических учреждений, но предупреждает, что распределение ресурсов может меняться в зависимости от спроса и будущих пожертвований.
Параллельно проект собирает партнёров для дополнительного обучения существующей открытой модели с более глубокой специализацией на математике. Это следующий этап разработки, а пока сервис работает с перечисленными готовыми моделями.
Наш канал в MAX
https://max.ru/mathematic
#Математика #ИскусственныйИнтеллект #Формализация #ОткрытыеМодели
По оценке команды проекта, эти модели примерно на год отстают от передовых по возможностям. От них не стоит ожидать решения сложных задач с одной попытки. Среди более реалистичных применений команда называет формализацию умеренного объёма в Lean, краткое изложение математических рассуждений и обсуждение математических тем.
Особенность платформы состоит в акценте на командных аккаунтах. Участники одной команды видят запросы друг друга. Разработчики предполагают, что такой формат может быть полезен для совместных проектов.
Вычислительные ресурсы предоставлены проекту в качестве пожертвований. Команда начала выдавать бесплатные аккаунты заявителям из академических учреждений, но предупреждает, что распределение ресурсов может меняться в зависимости от спроса и будущих пожертвований.
Параллельно проект собирает партнёров для дополнительного обучения существующей открытой модели с более глубокой специализацией на математике. Это следующий этап разработки, а пока сервис работает с перечисленными готовыми моделями.
Наш канал в MAX
https://max.ru/mathematic
#Математика #ИскусственныйИнтеллект #Формализация #ОткрытыеМодели
❤3👍1
Что значит классифицировать геометрические объекты? В алгебраической геометрии стремятся снабдить само множество классов геометрической структурой. Так возникает теория модулей. Её задача состоит в построении пространств, которые параметризуют изучаемые объекты. Классификация при этом сама становится предметом геометрии.
Классический пример дают гладкие кривые рода не меньше двух. Пространство их модулей допускает геометрическую компактификацию с помощью пространства модулей стабильных кривых. Здесь важно различать гладкие и стабильные кривые. Именно переход к стабильным кривым позволяет получить указанную компактификацию.
Построение этой теории стало итогом программы, начатой Риманом и развитой в работах Делиня, Гротендика и Мамфорда. Один из её инструментов, геометрическая теория инвариантов Мамфорда, использует факторизацию алгебраического многообразия по действию подходящей редуктивной алгебраической группы.
В более высоких размерностях важный поворот связан со статьёй Яноша Коллара и Николаса Шеперд-Баррона Threefolds and Deformations of Surface Singularities, опубликованной в 1988 году. В ней было предложено строить теорию многомерных пространств модулей методами бирациональной геометрии. Эта работа положила начало большой программе, включившей более 30 крупных статей Коллара и завершившейся его книгой Families of Varieties of General Type.
Наш канал в MAX
https://max.ru/mathematic
#АлгебраическаяГеометрия #ПространстваМодулей #Кривые #ИсторияМатематики
Классический пример дают гладкие кривые рода не меньше двух. Пространство их модулей допускает геометрическую компактификацию с помощью пространства модулей стабильных кривых. Здесь важно различать гладкие и стабильные кривые. Именно переход к стабильным кривым позволяет получить указанную компактификацию.
Построение этой теории стало итогом программы, начатой Риманом и развитой в работах Делиня, Гротендика и Мамфорда. Один из её инструментов, геометрическая теория инвариантов Мамфорда, использует факторизацию алгебраического многообразия по действию подходящей редуктивной алгебраической группы.
В более высоких размерностях важный поворот связан со статьёй Яноша Коллара и Николаса Шеперд-Баррона Threefolds and Deformations of Surface Singularities, опубликованной в 1988 году. В ней было предложено строить теорию многомерных пространств модулей методами бирациональной геометрии. Эта работа положила начало большой программе, включившей более 30 крупных статей Коллара и завершившейся его книгой Families of Varieties of General Type.
Наш канал в MAX
https://max.ru/mathematic
#АлгебраическаяГеометрия #ПространстваМодулей #Кривые #ИсторияМатематики
👍5
Может ли изначально регулярное течение жидкости за конечное время развить сингулярность?
Это один из центральных вопросов математической гидродинамики.
Уравнения Эйлера описывают движение невязкой несжимаемой жидкости. Эйлер опубликовал их в мемуаре 1757 года, и они относятся к самым ранним системам уравнений в частных производных в математической физике. Однако вопрос о возникновении сингулярностей продолжает направлять исследования спустя более двух с половиной веков.
Диего Кордоба и Луис Мартинес-Сороа в обзорном тексте обсуждают недавние математические работы и идеи построения решений с образованием сингулярности через каскад вихревых слоёв. Здесь важно сохранить точную постановку вопроса. Речь идёт об эволюции из первоначально регулярного состояния и о возможном возникновении сингулярности именно за конечное время.
Наш канал в MAX
https://max.ru/mathematic
#гидродинамика #уравненияЭйлера #сингулярности #матанализ
Это один из центральных вопросов математической гидродинамики.
Уравнения Эйлера описывают движение невязкой несжимаемой жидкости. Эйлер опубликовал их в мемуаре 1757 года, и они относятся к самым ранним системам уравнений в частных производных в математической физике. Однако вопрос о возникновении сингулярностей продолжает направлять исследования спустя более двух с половиной веков.
Диего Кордоба и Луис Мартинес-Сороа в обзорном тексте обсуждают недавние математические работы и идеи построения решений с образованием сингулярности через каскад вихревых слоёв. Здесь важно сохранить точную постановку вопроса. Речь идёт об эволюции из первоначально регулярного состояния и о возможном возникновении сингулярности именно за конечное время.
Наш канал в MAX
https://max.ru/mathematic
#гидродинамика #уравненияЭйлера #сингулярности #матанализ
🔥7🤡1🤣1
Начните с 2, 3, 5 или 7 и приписывайте по одной цифре справа так, чтобы на каждом шаге получалось простое число. Как долго можно продолжать?
В десятичной записи предел составляет восемь цифр. До этой длины доходят ровно пять чисел
23 399 339
29 399 999
37 337 999
59 393 339
73 939 133
У каждого из них любой начальный фрагмент, включая первую цифру, является простым числом. Но приписать справа ещё одну цифру и снова получить простое уже нельзя. Другие допустимые цепочки могут оборваться раньше, а до девятизначного числа не доберётся ни одна.
Наш канал в MAX
https://max.ru/mathematic
#ТеорияЧисел #ПростыеЧисла #Цифры
В десятичной записи предел составляет восемь цифр. До этой длины доходят ровно пять чисел
23 399 339
29 399 999
37 337 999
59 393 339
73 939 133
У каждого из них любой начальный фрагмент, включая первую цифру, является простым числом. Но приписать справа ещё одну цифру и снова получить простое уже нельзя. Другие допустимые цепочки могут оборваться раньше, а до девятизначного числа не доберётся ни одна.
Наш канал в MAX
https://max.ru/mathematic
#ТеорияЧисел #ПростыеЧисла #Цифры
🔥6👍3👏1
Формализация математики упирается уже в выбор определений. В проекте Annals Challenge Кевин Баззард ставит задачу записать на формальном языке формулировки всех теорем из недавних выпусков Annals of Mathematics, пока без доказательств. Главным препятствием здесь оказываются недостающие определения. Проект должен стимулировать создание формальных определений, которыми действительно пользуются исследователи.
Это помогает понять требования к большой математической библиотеке. Её понятия должны иметь ожидаемый математиком смысл, а связь с литературой должна позволять это проверить. Теоремы стоит формулировать достаточно общо для повторного использования, избегать дублирования, документировать и систематически организовывать материал. Именно такие принципы предлагают авторы эссе «How to Formalize All of Mathematics».
У машинной проверки есть конкретная задача. Lean позволяет проверять корректность формального доказательства. Но для дальнейшей работы с библиотекой важно также понимать, что именно доказано. Поэтому реестр проектов Palomar требует и метаданные с описанием формализованного результата и его происхождения, и настройку Comparator, облегчающую аудит точного утверждения.
Авторы эссе предлагают оценивать формализацию по тому, что она позволяет делать дальше. Можно ли с её помощью искать обобщения, исследовать связи между разделами, находить приложения, улучшать сами определения? В этой перспективе понятность, организация и возможность повторного использования входят в цель формализации с самого начала.
https://github.com/ImperialCollegeLondon/AnnalsChallenge
Наши каналы
MAX · Telegram · Дзен
#математика #формализация #доказательства #математическаялогика
Это помогает понять требования к большой математической библиотеке. Её понятия должны иметь ожидаемый математиком смысл, а связь с литературой должна позволять это проверить. Теоремы стоит формулировать достаточно общо для повторного использования, избегать дублирования, документировать и систематически организовывать материал. Именно такие принципы предлагают авторы эссе «How to Formalize All of Mathematics».
У машинной проверки есть конкретная задача. Lean позволяет проверять корректность формального доказательства. Но для дальнейшей работы с библиотекой важно также понимать, что именно доказано. Поэтому реестр проектов Palomar требует и метаданные с описанием формализованного результата и его происхождения, и настройку Comparator, облегчающую аудит точного утверждения.
Авторы эссе предлагают оценивать формализацию по тому, что она позволяет делать дальше. Можно ли с её помощью искать обобщения, исследовать связи между разделами, находить приложения, улучшать сами определения? В этой перспективе понятность, организация и возможность повторного использования входят в цель формализации с самого начала.
https://github.com/ImperialCollegeLondon/AnnalsChallenge
Наши каналы
MAX · Telegram · Дзен
#математика #формализация #доказательства #математическаялогика
🔥5❤1
Доски пяти гробов из южного Китая помогли восстановить историю засух перед падением Северной Сун. Исследователи изучили соотношение изотопов кислорода в древесных кольцах, охватывающих период 805–1150 годов.
В этой реконструкции доля тяжелого кислорода-18 служит показателем сухости условий, в которых росло дерево. Сопоставление колец разных лет указало на длительное снижение количества осадков с 1080-х годов. После 1101 года засушливость усилилась. При этом метод не позволяет точно определить величину изменений, поэтому превращать результат в конкретный процент сокращения осадков нельзя.
Исторические свидетельства дополняют эту картину. Они отмечают падение урожайности, сокращение распаханных площадей, массовую гибель цитрусовых деревьев в начале XII века и рост цен на рис. Государство пыталось сохранить налоговые поступления на фоне ухудшения экономического положения и военных конфликтов на севере.
Исследование поддерживает гипотезу, что многолетние климатические трудности существенно ослабили Сун перед потерей северного Китая в 1127 году. Это объяснение связывает изменения климата с состоянием сельского хозяйства и государственными финансами, сохраняя за климатом роль одного из факторов исторического кризиса.
Работа опубликована в npj Palaeoecosystems
https://www.nature.com/articles/s44513-026-00006-4
Наши каналы
MAX · Telegram · Дзен
#ИсторияКитая #Климат #Засухи #Изотопы
В этой реконструкции доля тяжелого кислорода-18 служит показателем сухости условий, в которых росло дерево. Сопоставление колец разных лет указало на длительное снижение количества осадков с 1080-х годов. После 1101 года засушливость усилилась. При этом метод не позволяет точно определить величину изменений, поэтому превращать результат в конкретный процент сокращения осадков нельзя.
Исторические свидетельства дополняют эту картину. Они отмечают падение урожайности, сокращение распаханных площадей, массовую гибель цитрусовых деревьев в начале XII века и рост цен на рис. Государство пыталось сохранить налоговые поступления на фоне ухудшения экономического положения и военных конфликтов на севере.
Исследование поддерживает гипотезу, что многолетние климатические трудности существенно ослабили Сун перед потерей северного Китая в 1127 году. Это объяснение связывает изменения климата с состоянием сельского хозяйства и государственными финансами, сохраняя за климатом роль одного из факторов исторического кризиса.
Работа опубликована в npj Palaeoecosystems
https://www.nature.com/articles/s44513-026-00006-4
Наши каналы
MAX · Telegram · Дзен
#ИсторияКитая #Климат #Засухи #Изотопы
🔥3👍1
«Graph Theory with Applications» представляет собой бесплатный вводный учебник по теории графов и её приложениям.
Изложение начинается с графов и подграфов, путей и циклов, деревьев и связности. Далее в книге рассматриваются эйлеровы и гамильтоновы графы, паросочетания, раскраска графов, планарные и ориентированные графы, сетевые потоки и экстремальная теория графов.
Авторы сочетают наглядное, геометрическое и топологическое понимание графов со строгим изложением математических основ. В описании книги среди областей применения этой теории названы информатика, компьютерные сети, оптимизация и анализ данных.
https://book.huihoo.com/pdf/graph-theory-with-applications.pdf
Наши каналы
MAX · Telegram · Дзен
#Математика #ТеорияГрафов #Геометрия #Топология #МатематическийАнализ
Изложение начинается с графов и подграфов, путей и циклов, деревьев и связности. Далее в книге рассматриваются эйлеровы и гамильтоновы графы, паросочетания, раскраска графов, планарные и ориентированные графы, сетевые потоки и экстремальная теория графов.
Авторы сочетают наглядное, геометрическое и топологическое понимание графов со строгим изложением математических основ. В описании книги среди областей применения этой теории названы информатика, компьютерные сети, оптимизация и анализ данных.
https://book.huihoo.com/pdf/graph-theory-with-applications.pdf
Наши каналы
MAX · Telegram · Дзен
#Математика #ТеорияГрафов #Геометрия #Топология #МатематическийАнализ
👍5
Что именно гарантирует проверка доказательства в Lean? Здесь важны три отдельных вопроса. Правильно ли сформулирована теорема, корректно ли проверено доказательство и насколько надёжна сама программа проверки.
Сначала Lean обрабатывает запись доказательства, проходя этап elaboration. Полученный результат проверяет ядро. Именно оно отвечает за проверку результата этой обработки. Написанный человеком или ИИ код доказательства ещё нельзя принимать на веру до проверки ядром.
Но даже успешная проверка требует человеческого аудита формулировки. Совпадает ли утверждение с той теоремой, которую собирались доказать? Соответствуют ли определения математическому замыслу? Томас Хейлс подчёркивает, что такой аудит обычно существенно проще проверки самого доказательства. Сведения о математике доступны на его университетской странице https://www.mathematics.pitt.edu/people/thomas-hales
У самой программы проверки тоже бывают ошибки. Особенно опасны ошибки логической корректности, позволяющие принять доказательство False. Из противоречия в используемой логике можно вывести любое утверждение, поэтому такой дефект разрушает смысл проверки.
Летом 2026 года при поиске уязвимостей Lean с помощью внутренних моделей OpenAI обнаружили ошибки в ядре и среде выполнения. Среди них были переполнение счётчика ссылок и использование версии библиотеки GMP с известной ошибкой. Обе уязвимости позволили добиться принятия доказательства False. В отчёте разработчиков указано, что Lean 4.33.1, выпущенный 21 августа, содержит исправления всех проблем, найденных в ходе этого поиска.
Подробности разобраны здесь https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/
Один из способов повысить доверие к результату состоит в повторной проверке независимыми программами. Однако несколько проверяющих могут содержать одинаковые или разные ошибки, приводящие к принятию одного некорректного доказательства. Поэтому важна независимость реализаций, а не только их количество.
Для потенциально вредоносных доказательств разработчики отдельно предупреждают, что обычного lake build недостаточно. Они рекомендуют comparator и внешние проверяющие программы. Это относится и к доказательствам, сгенерированным ИИ, которые в такой модели угроз рассматриваются как потенциально вредоносные.
Рекомендации по проверке https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-proofs
Инструмент comparator https://github.com/leanprover/comparator
Наши каналы
MAX · Telegram · Дзен
#матлогика #доказательства #верификация #основыМатематики
Сначала Lean обрабатывает запись доказательства, проходя этап elaboration. Полученный результат проверяет ядро. Именно оно отвечает за проверку результата этой обработки. Написанный человеком или ИИ код доказательства ещё нельзя принимать на веру до проверки ядром.
Но даже успешная проверка требует человеческого аудита формулировки. Совпадает ли утверждение с той теоремой, которую собирались доказать? Соответствуют ли определения математическому замыслу? Томас Хейлс подчёркивает, что такой аудит обычно существенно проще проверки самого доказательства. Сведения о математике доступны на его университетской странице https://www.mathematics.pitt.edu/people/thomas-hales
У самой программы проверки тоже бывают ошибки. Особенно опасны ошибки логической корректности, позволяющие принять доказательство False. Из противоречия в используемой логике можно вывести любое утверждение, поэтому такой дефект разрушает смысл проверки.
Летом 2026 года при поиске уязвимостей Lean с помощью внутренних моделей OpenAI обнаружили ошибки в ядре и среде выполнения. Среди них были переполнение счётчика ссылок и использование версии библиотеки GMP с известной ошибкой. Обе уязвимости позволили добиться принятия доказательства False. В отчёте разработчиков указано, что Lean 4.33.1, выпущенный 21 августа, содержит исправления всех проблем, найденных в ходе этого поиска.
Подробности разобраны здесь https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/
Один из способов повысить доверие к результату состоит в повторной проверке независимыми программами. Однако несколько проверяющих могут содержать одинаковые или разные ошибки, приводящие к принятию одного некорректного доказательства. Поэтому важна независимость реализаций, а не только их количество.
Для потенциально вредоносных доказательств разработчики отдельно предупреждают, что обычного lake build недостаточно. Они рекомендуют comparator и внешние проверяющие программы. Это относится и к доказательствам, сгенерированным ИИ, которые в такой модели угроз рассматриваются как потенциально вредоносные.
Рекомендации по проверке https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-proofs
Инструмент comparator https://github.com/leanprover/comparator
Наши каналы
MAX · Telegram · Дзен
#матлогика #доказательства #верификация #основыМатематики
👍3
Насколько хорошо число π можно приблизить дробями? Показатель иррациональности μ(x) измеряет качество рациональных приближений к числу x. Для любого иррационального числа он не меньше 2. Почти все действительные числа имеют показатель ровно 2, хотя существуют и числа с более высоким значением.
В препринте OpenAI «The irrationality exponent of π is 2», датированном 24 сентября 2026 года, заявлено равенство μ(π) = 2. Оно означало бы, что по этому показателю π относится к тому же классу, что и почти все действительные числа.
Здесь существенна именно точная величина показателя. Само по себе общее неравенство μ(x) ≥ 2 для иррациональных чисел ещё не даёт равенства для конкретного числа.
Текст препринта в PDF
https://github.com/openai/math/blob/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf
Наши каналы
MAX · Telegram · Дзен
#ТеорияЧисел #ЧислоПи #Иррациональность #Приближения
В препринте OpenAI «The irrationality exponent of π is 2», датированном 24 сентября 2026 года, заявлено равенство μ(π) = 2. Оно означало бы, что по этому показателю π относится к тому же классу, что и почти все действительные числа.
Здесь существенна именно точная величина показателя. Само по себе общее неравенство μ(x) ≥ 2 для иррациональных чисел ещё не даёт равенства для конкретного числа.
Текст препринта в PDF
https://github.com/openai/math/blob/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026/paper.pdf
Наши каналы
MAX · Telegram · Дзен
#ТеорияЧисел #ЧислоПи #Иррациональность #Приближения
❤4⚡1
Можно ли увидеть хаусдорфовость пространства на графе? Возьмём точки топологического пространства в качестве вершин. Две различные вершины соединим ребром, если у соответствующих точек нет непересекающихся открытых окрестностей.
Тогда пространство хаусдорфово в точности тогда, когда в этом графе нет рёбер. Это непосредственно следует из определения хаусдорфовости, которое требует для любых двух различных точек найти непересекающиеся открытые окрестности. Каждое ребро отмечает конкретную пару, для которой это требование нарушено. Так глобальное условие на пространство получает наглядное выражение через отношения между парами точек.
Подобный подход применим и к другим условиям отделимости, включая T₁, условие Урысона и функциональную хаусдорфовость. В работе П. Б. Винода Кумара с соавтором предложено рассматривать соответствующие графы как иерархию. Особенно естественен комбинаторный взгляд на конечные топологические пространства.
https://arxiv.org/abs/2602.00712
https://arxiv.org/abs/2610.14783
Наши каналы
MAX · Telegram · Дзен
#топология #теорияграфов #хаусдорфовость
Тогда пространство хаусдорфово в точности тогда, когда в этом графе нет рёбер. Это непосредственно следует из определения хаусдорфовости, которое требует для любых двух различных точек найти непересекающиеся открытые окрестности. Каждое ребро отмечает конкретную пару, для которой это требование нарушено. Так глобальное условие на пространство получает наглядное выражение через отношения между парами точек.
Подобный подход применим и к другим условиям отделимости, включая T₁, условие Урысона и функциональную хаусдорфовость. В работе П. Б. Винода Кумара с соавтором предложено рассматривать соответствующие графы как иерархию. Особенно естественен комбинаторный взгляд на конечные топологические пространства.
https://arxiv.org/abs/2602.00712
https://arxiv.org/abs/2610.14783
Наши каналы
MAX · Telegram · Дзен
#топология #теорияграфов #хаусдорфовость
❤2👍1
Лунные разломы позволяют оценить, насколько уменьшился радиус Луны. Ее недра остывают, и спутник сжимается. Под действием напряжений кора трескается, а ее участки наползают друг на друга, образуя уступы.
По снимкам Lunar Reconnaissance Orbiter планетологи нанесли на карту более 8900 тектонических разломов в высокогорьях и свыше 2600 небольших хребтов в лунных морях. Для оценки сжатия исследователи сопоставили размеры, форму, глубину залегания и общую протяженность разломов.
Полученная оценка суммарной деформации поверхности составляет 0,0048–0,0053%. Уменьшение радиуса авторы оценили в 42–46 метров за последние сотни миллионов лет. Это расчетная оценка по геологическим структурам.
Работа опубликована в The Planetary Science Journal.
https://iopscience.iop.org/article/10.3847/PSJ/ae9eae
Наши каналы
MAX · Telegram · Дзен
#геометрия #Луна #планетология
По снимкам Lunar Reconnaissance Orbiter планетологи нанесли на карту более 8900 тектонических разломов в высокогорьях и свыше 2600 небольших хребтов в лунных морях. Для оценки сжатия исследователи сопоставили размеры, форму, глубину залегания и общую протяженность разломов.
Полученная оценка суммарной деформации поверхности составляет 0,0048–0,0053%. Уменьшение радиуса авторы оценили в 42–46 метров за последние сотни миллионов лет. Это расчетная оценка по геологическим структурам.
Работа опубликована в The Planetary Science Journal.
https://iopscience.iop.org/article/10.3847/PSJ/ae9eae
Наши каналы
MAX · Telegram · Дзен
#геометрия #Луна #планетология
❤2⚡1