Hacker News Digest

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

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

Авторы ежедневно собирают и анализируют лексику из GitHub Pull Requests, чтобы выявить устойчивые паттерны в языке разработчиков. За 595 дней обработано более 461 тыс. PR и 51 млн слов, которые с помощью KL-дивергенции и k-means разбиты на 10 кластеров лексики. Один из кластеров, появившийся в 2026 году, доминирует в 40% всех PR, приписанных людям, за последний месяц, и его характерные слова напрямую связаны с использованием coding-агентов, таких как Claude Code.

Среди самых репрезентативных терминов этого кластера — load-bearing, refusal, survives, byte-identical, mutation-tested, structurally indistinguishable и другие, отражающие акцент на формальной верификации, неизменяемости и доказательной корректности кода. Эти слова указывают на сдвиг в практике разработки: всё больше PR фокусируются не на функциональности, а на гарантиях, которые код предоставляет — например, что изменение не ломает поведение, сохраняет битовую идентичность или выдерживает формальную проверку. Такой словарь стал «несущей конструкцией» современного кода, написанного с помощью ИИ-ассистентов.

Тред подтверждает наблюдаемость «клоудизмов» в проде и расширяет картину за пределы лексики: отмечаются синтаксические и форматные паттерны, проникновение в человеческую речь, гипотеза о компаундинг-эффекте при обучении новых моделей на AI-контенте, и практические попытки подавлять стиль через системные промпты. Отдельные респонденты считают часть слов обычным техжаргоном и оспаривают тезис о чисто LLM-происхождении слов типа load-bearing.

• Многие подтверждают из опыта, что «load-bearing», «spike», «sidecar», «resolver», «crux», «first-class citizen» массово появились в их кодовой базе и PR вместе с распространением Claude; @legobmw99 отмечает, что «sidecar» по их поиску стал использоваться в 3.6x чаще.

• LLM-лексика перетекает в человеческую речь: @nater5000 и @MrDrDr признаются, что стали непроизвольно использовать LLM-конструкции в своей письменной речи.

• Проблема выходит за лексику — синтаксис и формат тоже сигналят: @stabbles указывает на оборот «X contains no Y», @iamacyborg — на тирады с «, and», «, because», @elias_junit — на подчёркнуто линейную, хорошо структурированную подачу вместо нелинейного нарратива.

• Спор: Часть участников (@sethd, @danpalmer, @sosull) считает, что «Claude-измы» — это обычный техжаргон или следствие того, что модель буквально опирается на эти слова как на носители концептов (без них хуже думает), а @SalariedSlave и @polycaster, наоборот, видят именно LLM-специфичное явление и подозревают компаундинг-загрязнение обучающих данных.

• Совет: @ben30 показывает работающий приём: в глобальный промпт добавлено правило Орвелла и явный запрет на «load-bearing», «the crux», «first-class citizen»; в ответ Claude сам сообщает, что его системные инструкции требуют помечать «что-то load-bearing», то есть ограничение реально режет инструкции модели.

• Совет: @jimbobimbo использует в инструкциях агентов «find a synonym to 'resolve'», иначе появляется класс Resolver с методами ResolveThis/ResolveThat; @prmph заводит список запрещённых слов и просит переписать текст понятнее.

• Переломным по ощущениям @datadrivenangel называет примерно апрель (Opus 4.6/4.7), после чего Claude стал казаться «другим и более неудобным». @whywhywhywhy удивлён отсутствию в топе слова «shape».

• Подача проекта высоко оценена UX-составляющая: @nater5000 и @sosull хвалят, что всё помещается на экран без лишней воды, @Labo333 (автор) отвечает, что бэкенда нет — обновление и анализ делаются через GitHub Actions; обещает увеличить выборку до 1000 PR/день и поисковую строку.

Orwell's first rule: never use a metaphor you're used to seeing in print. "Load-bearing", "the crux", "first-class citizen" signal insight instead of showing it. Name the specific mechanism — @ben30

Архив Эдсгера Дейкстры содержит более тысячи его неопубликованных рукописей, известных как "EWDs", которые он рассылал десяткам получателей на протяжении более 40 лет. Дейкстра, один из основоположников компьютерных наук (1930-2002), внёс фундаментальный вклад в алгоритмы, языки программирования, операционные системы и формальную верификацию, за что получил высшую награду ACM - премию Тьюринга. Большинство его работ остались недоступными для широкой публики, пока не были оцифрованы и представлены на этом сайте в виде PDF-документов.

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

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

Ironclad — это формально верифицируемый, реального времени, UNIX-подобный ядро операционной системы общего назначения и встраиваемых систем, написанное на SPARK и Ada. Проект полностью свободный и распространяется под лицензией GPLv3. Ключевые особенности включают POSIX-совместимый интерфейс, одновременное вытесняющее многозадачность, обязательный контроль доступа (MAC) и поддержку жёсткого реального времени.

Главное преимущество Ironclad — формальная верификация с помощью SPARK для критических компонентов, таких как криптография и MAC. Система полностью портативна и зависит только от GNU toolchain, что упрощает кросс-компиляцию. Проект поддерживает дистрибутивы для всех доступных архитектур, наиболее заметный из которых — Gloire. Ironclad всегда будет бесплатным для использования, изучения и модификации, а финансируется за счёт пожертвований и грантов от NLnet и Европейской комиссии.

• Участники сомневаются в степени формальной верификации Ironclad, сравнивая его с более строгими аналогами вроде seL4 и Tock, и указывают на отсутствие доказательства ключевых свойств ядра.
• Проект написан на SPARK и Ada, поддерживает x86_64 и RISC-V, но не ARM64; его лицензия включает бесплатную версию с возможностью коммерческого использования.
• Основные альтернативы: seL4 (быстрый и строго верифицируемый), Genode (POSIX-совместимый слой), Asterinas и Redox (Linux-совместимые ядра), а также ReactOS и SerenityOS.
• Критика включает медленную производительность по сравнению с seL4, отсутствие capability-based безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.