Реестр, версия и фактический охват
Архивы распакованы отдельно, проверены чтением с контролем CRC. Пути проверены на выход за каталог; архивные скрипты не выполнялись. Контекст дедуплицирован по путям и SHA-256.
Архивы
| Архив | Размер, MiB | Текущих работ | Папок | PDF preprints | CRC |
|---|---|---|---|---|---|
| math_research_01_of_08.zip | 66.62 | 113 | 113 | 113 | OK |
| math_research_02_of_08.zip | 64.43 | 112 | 112 | 115 | OK |
| math_research_03_of_08.zip | 66.99 | 109 | 109 | 115 | OK |
| math_research_04_of_08.zip | 64.35 | 94 | 94 | 97 | OK |
| math_research_05_of_08.zip | 64.38 | 96 | 96 | 103 | OK |
| math_research_06_of_08.zip | 64.98 | 83 | 83 | 85 | OK |
| math_research_07_of_08.zip | 56.06 | 84 | 84 | 90 | OK |
| math_research_08_of_08.zip | 43.47 | 28 | 58 | 58 | OK |
Все 719 текущих ссылок из CONTENTS.md найдены; недостающих архивов серии 01–08 и текущих PDF нет. Числа семей по архивам могут пересекаться. Пропуски идентификаторов 045, 061, 070, 123, 163 — пропуски нумерации каталога, а не обнаруженные недостающие архивы.
SHA-256 каждого ZIP
math_research_01_of_08.zip5c735b4c234043dbff9be6dc7ea1d96dab0535f80607fd87d1dcb23073bbcd54
math_research_02_of_08.zip40a51f33992504fe2298832d269280bc82c12610885dc08dcac0e2c68cdc662c
math_research_03_of_08.zip3ca84563769b2e4f4276b6084989f9b0184d6fdd5ddb6edb4c5f4fc709e7d3ec
math_research_04_of_08.zipf63163e51eff12d62acae20421c7e382f0cca78ff33fcf062b6217fa1731420d
math_research_05_of_08.zipe81788815f68b83e57d8b96846c2b0f90571ba3a2f3aeede15ea181428659d13
math_research_06_of_08.zipe19b2af39873d8224d505e96914b0b2b8c6592288f7ae8acf5744aa88d9b90ac
math_research_07_of_08.zip15ad416aeec85684366a8fd8eba213dc8ff5277ea51b88bd02a4882fd9ace2ee
math_research_08_of_08.zip35b27de7b37216e399b06616e9acdeba418151e28855c83fc68b655b78453080
Какой объём действительно прочитан
| Операция | Охват | Чего она не означает |
|---|---|---|
| Каталожный разбор | 372 семьи, 719 текущих рукописей | Не чтение доказательств; у 358 семей применимость не оценена. |
| Структурное открытие PDF | 776 PDF, 36 694 страницы | Не просмотр всех страниц и не научная проверка. |
| Автоматическое извлечение текста выборки | 26 PDF, 1 208 страниц | Не прочтение 1 208 страниц. |
| Содержательный просмотр | 17 рукописей из 14 семей: вводные разделы, главные теоремы, планы доказательств | Не полный аудит; конкретные страницы записаны ниже. |
| Полное прочтение / проверка доказательства | 0 / 0 | Ни одна новая теорема не получила здесь сертификат корректности. |
| Формальные проверки | 0 запусков; 0 .lean в архивах | Описания охвата не равны исходной библиотеке. |
| Работа | Страницы PDF | Что просмотрено |
|---|---|---|
| 110-01 | 1–3 | Введение, теорема 1.1 и архитектура; доказательство целиком не прочитано |
| 110-02 | 1–2 | Теорема и оговорка о начальном периоде |
| 113-01 | 1–3 | Постановка, теорема, историческое сопоставление и оглавление доказательства |
| 115-01 | 1–3 | Теорема и начальная архитектура |
| 115-02 | 1–3 | Точная модель, история, отдельные последствия и конструкция больших ячеек |
| 118-01 | 1–4 | Модели LP, две главные теоремы, начальный план редукции |
| 121-01 | 1–4 | Аннотация, теорема, история и начало архитектуры |
| 124-01 | 1–4 | Постановка, теорема и описание ограниченных формул |
| 128-01 | 1–4 | Теорема, предшественники, графовая конструкция и начало леммы о вхождениях |
| 131-01 | 1–4 | Точное ядро, главная теорема, начало операторного сравнения; scope notes прочитаны |
| 139-01 | 1–4 | Оракульная модель, главные границы и архитектура |
| 325-01 | 1–3 | Главная теорема, предшественники, аналитическая схема |
| 003-01 | 4–6 | Главная теорема и обзор двух стадий; не полный текст |
| 003-02 | 2–3 | Главное утверждение и первые следствия |
| 032-01 | 1–4 | Главная теорема и геометрическая архитектура введения |
| 087-01 | 1–3 | Точная симметричная теорема и введение; компаньоны не разобраны |
| 109-01 | 1–4 | Модель, теорема и архитектура; 73-страничное доказательство не прочитано полностью |
Ключевые страницы локальных PDF дополнительно отрендерены для визуальной проверки формул; часть проверена на контактных листах. Это выборочный контроль чтения, не визуальный аудит всех страниц. Архивные reasoning_traces доступны: 10 PDF и один сопутствующий TeX. Они не использовались как доказательства и содержательно не изучались.
Что означает формальный каталог
В переданном контексте: 242 scope notes; formalization.yaml содержит 173 записи sources, 200 записей main_results и 30 related_formalizations; review.status — unchecked, scope — Partial progress. Авторы отдельно сообщают 300/719 top-line результатов. Эти числа считают разные сущности. Перестатейное сопоставление 300 результатов с декларациями и точными формулировками здесь не выполнено.
Исходный formalization.yaml · Локальная история · Что необходимо для настоящего формального аудита.
30 внекаталожных папок
Не входят повторно в 719. Все находятся в архиве 08. Для 27 неотозванных папок статус — «вне текущего каталога»; совпадение основы имени с текущей версией отмечено как кандидат, а не как проверенная смысловая эквивалентность.
Что не передано
Большая Lean-библиотека, исходники конкретных формальных доказательств, полноценный набор конфигураций Comparator и воспроизводимый запуск их проверок; независимые экспертные заключения для выбранных новых теорем; измерения новых алгоритмов на практических масштабах. Это ограничения материалов и выполненной работы, не вывод о ложности всех утверждений.
Структурированные партии: 01 · 02 · 03 · 04 · 05 · 06 · 07 · 08. Они содержат исходные пути и оговорки по каждой записи, а не только список заголовков.