ResearchТрудыПраці

DOI (Zenodo)

Lean proofsДоказательства LeanДокази Lean

The M024 archive contains Lean 4 files; a result is called certified only after a Lean 4.35.0 check without sorry. Per-theorem pages will appear with the monograph.Архив M024 содержит файлы Lean 4; результат считается подтверждённым только после проверки Lean 4.35.0 без sorry. Страницы по теоремам появятся вместе с монографией.Архів M024 містить файли Lean 4; результат вважається підтвердженим лише після перевірки Lean 4.35.0 без sorry. Сторінки з теорем з’являться разом з монографією.

How we present resultsКак мы подаём результатыЯк ми подаємо результати

Lean blueprints show a theorem → Lean-code graph. We add the following by design; none of it is claimed as novel until compared with the literature.Lean blueprint даёт граф «теорема → код Lean». Мы добавляем по замыслу то, что ниже; новизна не заявляется до сравнения с литературой.Lean blueprint дає граф «теорема → код Lean». Ми додаємо за задумом те, що нижче; новизна не заявляється до порівняння з літературою.

• Status / Статус: LEAN · TWO CHECKS · ONE CHECK · CONJECTURE · REFUTED · KNOWN.
• Provenance pipeline: conjecture → recomputation → independent certification → Lean → literature. An AI answer is data, not proof.Конвейер: гипотеза → пересчёт → независимая сертификация → Lean → литература. Ответ ИИ — данные, не доказательство.Конвеєр: гіпотеза → перерахунок → незалежна сертифікація → Lean → література. Відповідь ШІ — дані, а не доказ.
• “Proved” requires two independent checks (outside Lean).«Доказано» требует двух независимых проверок (кроме Lean).«Доведено» потребує двох незалежних перевірок (крім Lean).
• Refuted claims are kept and shown, with the reason.Опровергнутое хранится и показывается, с причиной.Спростоване зберігається і показується, з причиною.
• Lean trust boundaries stated explicitly (kernel vs native_decide, axioms) plus a “not verified” list.Границы доверия Lean указаны явно (ядро и native_decide, аксиомы) и список «не проверено».Межі довіри Lean вказані явно (ядро і native_decide, аксіоми) та список «не перевірено».
• Priority gate: “known / close / not found” with an exact reference — never “new” by default.Гейт приоритета: «известно / близко / не найдено» с точной ссылкой — «новое» по умолчанию не пишем.Гейт пріоритету: «відомо / близько / не знайдено» з точним посиланням — «нове» за замовчуванням не пишемо.
• Reproducibility: command + sha256 + receipt per artifact.Воспроизводимость: команда + sha256 + квитанция у каждого артефакта.Відтворюваність: команда + sha256 + квитанція в кожного артефакта.

Literature and prior artЛитература и прототипыЛітература та прототипи

Reviews are stored in the repository; novelty is claimed only after a literature check.Разборы лежат в репозитории; новизна заявляется только после проверки литературы.Огляди лежать у репозиторії; новизна заявляється лише після перевірки літератури.