Hacker News Digest

Клод, ИИ-модель от Anthropic, за 11 дней автономно создал первое полностью компьютерно проверенное доказательство Великой теоремы Ферма в системе доказательств Lean. Он написал 13 миллионов строк кода и доказал 29 500 промежуточных теорем, охватив алгебру, гармонический анализ, геометрию и теорию чисел. Это достижение подтверждает, что теорема верна исключительно на основе аксиом математики, без дополнительных предположений. Кевин Бззард отметил, что доказательство многослойное и достаточно надёжное, чтобы служить основой для дальнейших исследований. Автоматическая формализация таких сложных доказательств открывает путь к будущему, где любые математические результаты можно будет быстро и надёжно верифицировать, снижая нагрузку на сообщество при оценке новых работ. Это особенно важно, учитывая историю ошибок в математике — от сотен ложных попыток доказать FLT до летних споров вокруг доказательств гипотез Пуанкаре и Голдбаха. Теперь ИИ может помочь сделать математику более прозрачной и доверенной.

Формализация Великой теоремы Ферма в Lean знаменует сдвиг в методологии математики, требуя пересмотра доверия к проверке, масштабу и воспроизводимости доказательств. Контекст проекта можно уточнить в блоге Кевина Баззарда (Imperial College), а исторический фон — в книге Саймона Сингха. Доказательство охватывает только случай p≥17; для меньших простых теорема уже доказана. Объём кода (~13 млн строк) вызывает сомнения в полной безошибочности: ядро Lean ранее уже имело эксплуатируемые уязвимости, что создаёт риск скрытых ошибок. Некоторые считают такой код «чёрным ящиком» — нечитаемым в отличие от человеческих доказательств. Стоимость формализации составила ~$300k по тарифам API, что делает проекты экономически осуществимыми, но не массовыми. Платформа Prove2Me показала, что человеческие инструменты критически важны и при автономной работе ИИ. Часть кода предлагается внести в Mathlib, чтобы сохранить вклад для сообщества. Для будущих формализаций рекомендуют Metamath с его минимальным ядром проверки. Для масштабных проектов потребуются системы управления задачами (например, JIRA), а для изучения Lean — качественный учебник, так как текущие ресурсы недостаточны. Достижение показывает, что ИИ способен формализовать сложнейшие теоремы (включая потенциальную классификацию конечных простых групп) и синтезировать конструкции за пределами существующих библиотек. Это снижает нагрузку на рецензентов, однако формализация не опровергает оригинальное доказательство Уайлса, а лишь подтверждает его строгой логикой, не заменяя человеческого понимания.

Теренс Тао, один из ведущих математиков современности, выделяет шесть фундаментальных концепций, которые лежат в основе математического мышления. Первое — это числа и их свойства, включая натуральные, целые, рациональные и иррациональные числа, которые формируют основу для арифметики и алгебры. Второе — структура и симметрия, проявляющиеся в геометрии и теории групп, где понимание инвариантности помогает решать сложные задачи. Третье — функции и зависимости между переменными, которые моделируют реальные процессы от физики до экономики. Четвёртое — доказательство как строгий метод обоснования истинности утверждений, отличающее математику от других наук. Пятое — абстракция и обобщение, позволяющие выделять общие паттерны из конкретных примеров, например, переход от конкретных уравнений к теории уравнений. Шестое — применение математических идей в других областях науки и техники, демонстрирующее их универсальность и практическую ценность. Тао подчеркивает, что mastery этих концепций не требует гениальности, а скорее любопытства, настойчивости и готовности думать логически и креативно одновременно. Он также отмечает, что ошибки и неудачи — неотъемлемая часть обучения, и что настоящее понимание приходит не от запоминания формул, а от глубокого осмысления лежащих в их основе идей. Эти шесть столпов, по его мнению, формируют не только математическую грамотность, но и способность ясно и структурированно мыслить в любой области жизни.

Видео Т. Тао помогает понять фундаментальные идеи математики: большинство зрителей отмечают рост уверенности в сложных темах. Предложения: - Заменить «Геометрию» на «Топологию», добавить логику и теорию типов как более современные фундаментальные области. - Изучить теорему перестановки Римана как пример неожиданного поведения бесконечных рядов. - Прочитать «How to Solve It» Джорджа Поля для развития математического мышления. Связь с практикой: несколько комментаторов сопоставляют шесть концепций с разработкой — понимание, верификацию и синтез в математике сравнивают с генерацией кода и проверкой программ. Дополнительные ресурсы: видео 3Blue1Brown, «The Joy of X» Стивена Строгацса, предзаказ книги Тао «Six Math Essentials». Споры: - Аналогия с обезьяной, пишущей «Гамлета», критикуется как упрощённая: один пользователь считает, что она недооценивает нелинейность обучения, другой указывает, что сравнивается лишь вывод, а не понимание. - Происхождение термина «irrational»: один комментатор считает соотнесение с «безумным» странным, другой приводит этимологию, отмечая, что математическое значение существует с XIV века. Таким образом, обсуждение дополняет статью реальными отзывами, рекомендациями и небольшими спорами.

Искусственный интеллект не «умнее» математика — он просто помнит в разы больше. В отличие от человека, чья рабочая память удерживает лишь несколько абстрактных элементов одновременно, нейросети могут удерживать в контексте тысячи формул, промежуточных выводов, определений и даже отброшенных подходов. Это позволяет решать сложные задачи, не перегружая биологические ограничения.

Ключевой факт: человеку трудно умножить в уме два трёхзначных числа — не из-за сложности операций, а из-за необходимости одновременно хранить промежуточный результат и текущую цель. Бумага или цифровой контекст устраняют эту «узкую горлышко» интеллекта. Математики используют нотацию, схемы и «чанкинг» (группировку знакомых конструкций), чтобы компенсировать лимит памяти, но не преодолевают его. AI же работает с внешним «бесконечным блокнотом», где каждый шаг фиксируется. Это делает его похожим на машину-умножитель Вон Неймана: не гениальный в философском смысле, но способный обрабатывать масштабы, недоступные мозгу.

Запомните: рабочая память — главный барьер для человеческого математического мышления. Её объём напрямую коррелирует с успехом в математике, независимо от общего ИК. Но у AI нет «глубины» Вон Неймана — он лишь использует его скорость и объём памяти как инструмент. Следующий прорыв наступит, когда ИИ поймёт, что задача сформулирована неверно, и переосмыслит её фундаментально.

Пример: Чтобы доказать теорему о сходимости ряда, математик может одновременно удерживать в голове 5 определений, 3 предыдущих леммы и текущую цель. AI же хранит все эти элементы в контексте и перебирает варианты, не уставая.

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

OpenAI представил десять прорывных результатов в математике и теоретической информатике, полученных с помощью внутренней версии модели Astra. Среди них — новые верхние оценки плотности упаковки сфер в высоких размерностях, достигнутые вплоть до порога Коэна–Элкиса, и экспоненциально улучшенные границы для максимального размера двоичных кодов при заданном минимальном расстоянии. Также решены задачи в теории кодирования, сложности арифметических схем, квантовой сложности и решёточной криптографии. Все доказательства были формализованы в системе Lean и сопровождаются пошаговыми объяснениями модели.

Общая стоимость вычислений для нахождения решений составила около $2000 по тарифам Sol API. Каждое решение сопровождается аудио-навигацией мышления модели и человеческой редактурой. Это первый масштабный пример, когда ИИ не просто помогает, а самостоятельно открывает новые математические истины, которые затем формализуются и проверяются. Результаты опубликованы в открытом доступе вместе с Lean-сертификатами, что позволяет сообществу воспроизводить и развивать их. Такой подход меняет роль ИИ с инструмента поддержки на соавтора научных открытий.

Скептическая оценка маркетинга OpenAI: результаты — не фундаментальный прорыв, а эффективный перебор известных методов без новой математики. AI не обладает интуицией, не формулирует гипотезы, но превосходит людей в рутинном вычислительном переборе, превращая доказательства в вычислительные задачи. Стоимость $2000 вводит в заблуждение: скрытый масштаб экспериментов (p-value hacking) и низкая загрузка мощностей искажают реальную цену. Отсутствует прозрачность: неизвестно число попыток, объяснения содержат логические скачки, затрудняющие проверку. Lean-доказательства достигают 50k строк, но стиль изложения слаб. Настоящий прорыв наступит, когда AI создаст новую ветвь математики — пока лишь усиливает внимание к существующим областям. Ускорение решения задачи ближайшего вектора угрожает криптографии, что уже учитывается переходом на гибридные схемы. Практического применения в медицине или материаловедении пока нет. Тревога по поводу разрушения академической системы: если AI решит задачи, лежащие в основе научных карьер, это подорвёт финансирование и престиж. Ирония: заявление OpenAI о «ответственности за корректность» доказательств сравнивают с добровольным статусом козла отпущения.

Каждый несвязный без мостов граф содержит набор циклов, покрывающих каждую дугу ровно дважды. Для доказательства достаточно рассмотреть кубические (3‑регулярные) графы без мостов. Такие графы всегда обладают ничтожным 8‑потоком, что эквивалентно наличию ничтожного потока над полем Γ=𝔽₂³. На основе этого потока строится раскладка ребер множествами из двух элементов Γ так, чтобы у каждой вершине каждый элемент Γ встречался либо 0, либо 2 раза. Эта «расслабленная» 3‑красочная раскладка приводит к требуемому покрытию.

Для каждой вершины локально выбираются три элемента Γ из значений потока на её трёх инцидентных ребрах; из них формируются пары {t, t+x}, {t+x, t+z}, {t, t+z}. На каждом ребре эти пары совпадают, если выполнена система линейных уравнений над Γ⊕𝔽₂, которая всегда имеет решение (лемма 2.2). После выбора параметров t_v и ε_e получаем для каждого ребра набор из двух элементов Γ, удовлетворяющий условию (1). По построению множества M_s={e:s∈P_e} разбиваются на циклы, каждый элемент Γ появляется в ровно двух M_s около любой вершины, а их объединение покрывает все ребра двойным циклом. Таким образом любой безмостовой граф имеет цикл‑двойное покрытие.

• ИИ создал короткое доказательство задачи о двойном покрытии циклов, которое прошло проверку.
• Промпт включал множество метаинструкций и требовал от модели «продолжать» работу.
• Реакция сообщества разнообразна: от восхищения до скептицизма по поводу проверки и значимости.
• Ключевой вопрос — необходимость независимого математического рецензирования и прозрачности процесса.

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

Подсознательная обработка проблем после интенсивной работы над ними приводит к "озарению" - внезапному появлению решения после периода бессознательного инкубации. Однако Адамар описывал иной процесс: математики сознательно, но без слов удерживали проблему в центре внимания, используя метафорические образы (как "лента переменной толщины" для бесконечных рядов). Это позволяет направлять ментальные ресурсы на решение важных задач, превращая подсознание в бесплатного ассистента.

• Люди с нейродивергентным мышлением описывают мыслительный процесс как визуальный, а не вербальный, что вызывает вопросы о том, как они вообще формулируют и передают идеи без слов.
• Среди участников обсуждения есть те, кто считает, что мышление без слов — это нечто, что может быть развито у любого человека, и что это может быть полезно для решения проблем.
• Обсуждается, что мышление без слов может быть полезно для решения проблем, но также может быть трудно выразить эти мысли словами.
• Участники обсуждения также затрагивают вопрос о том, как мыслительный процесс может влиять на способность к обучению и решению проблем.

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

Этот метод применим к любым вращающимся объектам: спинам, кубитам, гироскопам и роботизированным рукам. Даже если объект прошел сложную траекторию, масштабирование всех углов вращения на один и тот же коэффициент и повторение этой траектории дважды возвращает его в исходное положение. Математическое доказательство основано на каталоге всех возможных вращений в трехмерном пространстве, известном как SO(3), который описывается с помощью абстрактного математического пространства, структурированного подобно шару.

• Обсуждение вращений в SO(3) и SU(2) показало, что любой путь вращений можно «сбросить» в исходную точку, если повторить его дважды с подходящим масштабным коэффициентом λ, но формула для вычисления λ пока неизвестна.
• Работа Эккмана и Тлусти подчеркивает, что классическая механика допускает обратимость, но не даёт способа вычислить обратную последовательность вращений без полного перебора всех возможных.
• Исследование вращений в контексте робототехники, МРТ и квантовых вычислений подчеркивает, что вращения в 3D-пространстве могут быть «сброшены» с помощью простой последовательности шагов, но неясно, как вычислить эту последовательность.
• Обсуждение также затрагивает вопрос о том, можно ли применить этот результат к «сбросу» любой последовательности вращений в контексте робототехники и МРТ, и поднимает вопрос о том, что такое вращение в контексте квантовых вычислений.

Линейная алгебра начинается с двух ключевых идей: метода Гаусса и концепции строкового и столбцового представления. На примере монет: уравнение 5x + y = 23 (где x — никели, y — пенни) имеет несколько решений, например, 4 никеля и 3 пенни или 23 пенни. Это линейное уравнение, так как его график — прямая.

Сложность возникает, когда переменных две, но нужно удовлетворить двум условиям. Например, в задаче о питании: молоко (1 г углеводов, 2 г белка) и хлеб (2 г углеводов, 1 г белка). Чтобы получить 5 г углеводов и 4 г белка, нужно решить систему из двух уравнений. Метод Гаусса позволяет найти такие x и y, которые одновременно удовлетворяют обоим уравнениям, демонстрируя переход от одной переменной к системам.

• Пользователи высоко оценили визуальный стиль и доступность объяснений в блоге, сравнивая его с другими популярными ресурсами.
• Было высказано пожелание начинать объяснение линейной алгебры с практической задачи и графической интерпретации, а не с абстрактного метода (как Gaussian elimination).
• Обсуждалась цель изучения линейной алгебры: для практического применения или глубокого теоретического понимания.
• Отмечены технические проблемы с отображением иллюстраций в тёмном режиме на iOS Safari.
• Упомянуты другие учебные материалы по теме и выражена благодарность автору за качественный контент.

Фурье-преобразование — это способ разложить любую функцию на сумму простых волн.

Идея родилась в 1807 г., когда Жан Батист Жозеф Фурье искал закон теплопроводности. Он показал: любая периодическая кривая — это набор синусов и косинусов с разными частотами и амплитудами.

Современная формула
$$ \hat f(\xi)=\int_{-\infty}^{\infty} f(x),e^{-2\pi i x\xi},dx $$
переводит сигнал из «временной» области в «частотную».

Как работает

• Сложный звук → набор чистых тонов.
• Изображение → сетка синусоидальных полос разной плотности.
• Удалив высокие частоты, получаем сжатие JPEG; убрав низкие — оставляем контуры.

Применения

• МРТ и рентген: преобразование Радона + обратное Фурье.
• Сотовая связь, радары, шумоподавление.
• Решение дифференциальных уравнений и квантовая механика.

Интуиция
Фурье-анализ — это «математический слух»: он выделяет, какие «ноты» содержатся в любом сигнале.

• В треде делятся ссылками на яркие визуализации: Captain Disillusion, 3Blue1Brown, MIT-лекция Фримена, интерактивы injuly.in и jezzamon.
• Кто-то предупреждает: «простые» объяснения могут дать иллюзию понимания, лучше сразу смотреть на математику.
• Появляются любители Лапласа/z-преобразования, жалуются, что о них почти нет популярных видео.
• Обсуждают практику: JPEG, OFDM, сжатие манги, анти-муар, фильтры в е-ink, а также «почему это работает» — спarsity, смена базиса в бесконечномерном пространстве.
• Интересуются деталями: как выбрать частоты, как считать преобразование на потоке, почему убрать высокие частоты = размытие.

Репозиторий the-litte-book-of/linear-algebra на GitHub.
Эпиграф Жана Дьёдонне: «Линейная алгебра — почти самая элементарная теория, хотя преподаватели и авторы учебников на протяжении поколений затемняли её простоту чудовищными выкладками с матрицами».

Меню навигации, вход, настройки внешнего вида, поиск и другие стандартные элементы GitHub опущены.

• Линейная алгебра считается глубокой и полезной, но базовая механика скучна.
• Многие советуют начинать с геометрической интуиции и визуализации (3Blue1Brown, «Wild Linear Algebra», mini-book photon_lines).
• Книга Axler «Linear Algebra Done Right» и курс Hefferon хвалятся за строгий, но понятный подход.
• Практика в графике/3D, экономике, машинном обучении и сжатии JPEG делает тему мотивирующей.
• Сообщество жалуется на плохое преподавание и просит больше визуальных объяснений, меньше «так надо».

Румыния — малый 19-миллионный балканский государство — регулярно входит в мировую пятёрку по математическим, физическим и информатическим олимпиадам, несмотря на посредственные средние результаты PISA и симметричное распределение способностей. Объяснение кроется в уникальной структуре образования.

После войны коммунисты 1948 г. за десятилетие ликвидировали неграмотность, построив сеть доступных, хотя и примитивных школ по советскому образцу. После 1989 демократические власти закрыли лишние здания, но сохранили жёсткий отбор: уже в начальной школе выявляют способных и направляют в специализированные лицеи и гимназии с углублённой подготовкой. Эти узкие «олимпиадные трубы» концентрируют ресурсы, лучших учителей и соревновательную культуру, порождая крошечную, но мощную элиту, которая и приносит стране медали.

• Румынская система образования жёстко сортирует учеников: лучших собирают в «национальные колледжи» с лучшими учителями и максимальной поддержкой олимпиадного движения.
• Это даёт высокие места на IMO, но за счёт остальных школьников и приводит к оттоку талантов за границу.
• Похожие советские/соц-школы были и в Венгрии, Болгарии, России, но после 1990-х их качество упало, а румынская модель сохранилась.
• Критики обвиняют автора статьи (Jordan Lasker) в расистской риторике и псевдонауке, советуют относиться к выводам осторожно.
• Итог: стратифицированная система создаёт узкий пул звёзд-олимпиадников, но не повышает общий уровень математики в стране.

Бог создал действительные числа, а не целые.
16-вековая Италия считала науку знанием о вечном, созданном Богом, а искусство — делом человеческим. Кронекер утверждал: «Бог сотворил целые, всё остальное — дело рук человеческих». Но целые слишком просты и элегантны, чтобы быть «божественными»; природа не стремится к абстрактной простоте. Настоящая «божественная» математика — это иррациональные, «тошнотворные» действительные числа: √2, π и прочие бесконечности, вызывающие у человека головокружение.

Иерархия странности
Вечная природа → природа → люди → человеческие идеи. Чем ближе к вечной природе, тем выше степень странности. Целые числа лежат ближе к человеческим идеям, поэтому кажутся «совершенными»; молоток кажется идеальным инструментом, потому что был изобретён людьми для людей.

Кронекер, Кантор и Бог
Кронекер атаковал бесконечность, чтобы защитить «божественные» целые. Кантор же видел в трансфинитах путь к Богу и полагал, что математика — это Бог, говорящий через него. Гильберт назвал «рай Кантора» неизгладимым.

• Участники спорят, «естественны» ли вещественные числа или это всего лишь удобная человеческая абстракция.
• Некоторые склоняются к финитизму: природа дискретна, а непрерывность — модель, не имеющая физического подтверждения.
• Другие считают, что математика изобретена, но полезна: «карта не есть территория», и бесконечности не нужны для описания мира.
• Обсуждаются комплексные, рациональные и даже «мнимые» числа как примеры конструкций, которые кажутся «реальными», лишь пока мы ими пользуемся.

JavaScript отключён
Включите JavaScript или перейдите в поддерживаемый браузер.
Список браузеров — в Справке.

Попробуйте снова
⚠️ Расширения, связанные с приватностью, могут мешать работе x.com. Отключите их и обновите страницу.

• Утверждение «GPT-5 Pro доказал новую интересную математику» вызвало споры: кто-то считает это прорывом, кто-то — переоценкой.
• Критики указывают, что улучшенная теорема уже была доказана людьми в апреле, а сам результат не революционен.
• Сомнения вызывает и методология: неясно, сколько попыток потребовалось, чтобы получить «удачный» вывод.
• Математики подчеркивают: генерация формул ≠ строгое доказательство; важны семантика и проверка.
• Параллельно всплыли примеры из других областей (поиск лекарств, антенны NASA), где ИИ «открывает» известное, но упущенное людьми.
• Общий вывод: ИИ может помогать в математике, но пока это скорее инструмент для ускорения, чем источник глубоких новых теорий.

Как двигать объекты в 3D

Кликните вправо, чтобы идти дальше →

---

От круга к сферической спирали

Куб движется по кругу:
x = 10 cos(πt/2)
y = 10 sin(πt/2)

Умножаем радиус на 0.03 t — получаем растущую спираль.

---

Сферическая спираль

Добавляем z:
z = 10 cos(0.02 πt)

Радиус x, y теперь умножается на sin(0.02 πt), поэтому он сначала растёт, потом уменьшается.

x = 10 cos(πt/2) · sin(0.02 πt)
y = 10 sin(πt/2) · sin(0.02 πt)
z = 10 cos(0.02 πt)

Куб облетает сферу по спирали.

---

Итог

Положение в 3D задаётся параметрическими уравнениями x(t), y(t), z(t).
Меняя функции, получаем любые траектории — от простого круга до «хаотичных» путей.

Проект Damar • Twitter @damarberlari

• Пользователи восторгаются плавной анимацией и наглядностью объяснения сферической спирали.
• Некоторые жалуются на тормоза в Firefox/Linux и просят убрать «диззи»-эффект.
• Просят добавить навигацию свайпом/скроллом, кнопки «вперёд-назад» и RSS-ленту.
• Отмечен скачок сложности: от азов к финальной спирали — слишком большой шаг для новичков.
• Появились предложения расширить тему: полярные координаты, матрицы поворота, Fibonacci-спираль на сфере.