Корректность новых доказательств
Полные доказательства не прочитаны и не проверены построчно. Изучены только конкретно перечисленные страницы 17 рукописей. Подробный разбор постановки не равен рецензии.
Что пока не подтверждено
Сайт различает утверждение рукописи, описание формального охвата, внешнюю работу-предшественник и собственный маленький эксперимент. Эти уровни не объединяются в один балл «доверия».
Реальное формальное покрытие
Ни одного .lean-файла в переданных архивах нет. Не запущены Lean, Comparator, аудит аксиом или проверка соответствия формулировок. В группе 131 scope note исключает точный sampler, хотя охватывает оценку смешивания.
Независимая экспертная проверка
В выполненном ограниченном поиске не установлено независимое подтверждение именно выбранных новых главных утверждений. Найдены первичные предшествующие работы; они не являются рецензиями этой коллекции.
Практическая эффективность
Не воспроизведены новые большие алгоритмы. Восемь браузерных опытов — точные малые эталоны, известные методы или расчёт формулы. Нет выдуманных данных о скорости, точности или выручке.
Полнота зависимостей
Показаны несколько подтверждённых связей из каталога, введений и уведомлений. Полный граф логических зависимостей 719 рукописей не восстановлен. Библиографическая ссылка сама по себе не доказывает зависимость.
Смысл всех каталожных записей
Для 358 семей нет индивидуального научного обзора. Русские заголовки — перевод, тип результата предварителен, заявленный результат хранится в оригинале; прикладная близость не назначена искусственно.
Отзыв: конкретный сбой и две зависимые работы
Локальный history.md фиксирует 07.10.2026 отзыв «Algebraicity of Weil classes on split abelian eightfolds» и двух зависимых рукописей. Их README датируют сам отзыв 06.10.2026. Это различие дат сохранено, а не сглажено.
Стрелка: входная конструкция используется в зависимом доказательстве. Отзыв доказательства не означает ложности самой теоремы. Текущая CM-работа 032 не отождествляется с этой конструкцией без проверки.
В чём именно ошибка
README объясняет: при принятом соглашении исходное алгебраическое число двойных точек равно −m. Обратной стабилизации приписывался знак +1, но ориентации дают −1. В результате получается −2m, а не 0. Требуемая гипотеза операции устранения двойных точек не выполнена. Здесь проверено уведомление об ошибке; самостоятельный геометрический аудит не проводился.
Algebraicity-of-Kuga-Satake-Correspondences-for-K3-Surfaces-October-3-2026: уведомление об отзывеmath_sources/math_research_08_of_08/preprints/Algebraicity-of-Kuga-Satake-Correspondences-for-K3-Surfaces-October-3-2026/README.md
The-rational-Hodge-conjecture-for-products-of-K3-surfaces-October-4-2026: уведомление об отзывеmath_sources/math_research_08_of_08/preprints/The-rational-Hodge-conjecture-for-products-of-K3-surfaces-October-4-2026/README.md
Algebraicity-of-Weil-classes-on-split-abelian-eightfolds-September-18-2026: уведомление об отзывеmath_sources/math_research_08_of_08/preprints/Algebraicity-of-Weil-classes-on-split-abelian-eightfolds-September-18-2026/README.md
Несколько других зависимостей
| Вход → использующее утверждение | Тип связи и источник | Что нельзя заключить |
|---|---|---|
| 032 → 001 | Каталог явно связывает рациональность Милна с результатом CM-Hodge; CONTENTS.md, запись 001. | Два заголовка не означают два независимых доказательства. |
| 006 → 002 | Каталог указывает использование результата семьи 006 в BSD-формуле; запись 002. | Полный набор гипотез не восстановлен по одной ссылке. |
| 110-01 → 110-02 | Абстрактная конкурентная теорема → вычислительная реализация; 110-02, с. 1. | Полиномиальность не устраняет огромный запуск и аддитивную цену. |
| 113-01 → расширение, обсуждаемое в 131 | 131, с. 2–3, ссылается на 113-01, следствие 10.1, для подграфов ограниченного host-графа. | Это не зависимость основной switch-оценки и не доказательство её для ограниченного host-графа. |
Восемь проведённых вычислительных опытов
Перечислено 70 графов с заданными степенями; проверены целые веса ядра и его симметрия. Для полей [3,3], [2,2,2] перечислены семь таблиц. Независимым вычислением нормы проверены аналитические 2×2 примеры. Для малого SCS и расписаний получены точные эталоны. Браузер дополнительно проверяет динамику edit distance и полярные площади. Результаты сохранены, а алгоритмы доступны в исходном коде.
Скрипт — созданный для этого атласа, не из архива. Требует Python и NumPy; установка зависимостей не выполняется автоматически. Время исполнения новых алгоритмов не измерялось.
Следующие шаги настоящей проверки
1. Зафиксировать вход. Получить точный commit полной Lean-библиотеки и зависимости; сверить хеши с используемой версией PDF.
2. Сопоставить формулировки. Для каждой выбранной теоремы выписать гипотезы и вывод формальной декларации; проверить, не формализована ли только вспомогательная лемма.
3. Запустить проверку. В изолированной среде выполнить компилятор, Comparator и аудит аксиом/заглушек; сохранить лог, версию инструмента и список импортов. Один успешный build не решает задачу смыслового сопоставления.
4. Проверить главные узкие места. Некоммутирующие проекции в 131; масса и редкая коррекция в 115; матричный порядок произведений в 325; компактные описания в 124; равномерные аналитические запасы в 003.
5. Только затем оценивать внедрение. Реализовать алгоритм без подмены известной эвристикой; измерить подготовку, память, точность и хвосты времени. Рыночный спрос проверять отдельным пилотом.