Блог
Я проверил машиной восемь своих теорем. Четыре устояли, три заголовка были неверны
Каждая теорема свода перепроверена против собственного доказательства. Четыре устояли. Одна сузилась, одна перестала быть теоремой, одна оказалась дубликатом другой.
Подписи на изображении — на английском.
- EIGHT THEOREMSFour held as standard results.
- THE MACHINETwo passes disputed no verdicts.
- THE HEADINGSThree headings overstated their results.
Свод содержал восемь пронумерованных теорем. Я перечитал каждую против её доказательства, не против памяти о ней. Четыре устояли без правок.
Теорема 4 — сужена
Утверждение было сформулировано для всех элементов. Доказательство молча предполагало обратимость: ноль аннулирует произведение, и шаг, делящий на него, неверен ровно в этой точке.
Теорема осталась истинной; ложной была её область. Сужение — это не отзыв, а восстановление той границы, внутри которой доказательство действительно работает.
Практической разницы почти нет: нулевой элемент в этом контексте почти не встречается. Но «почти не встречается» — свойство входных данных, а не теоремы, и потому не может стоять в её формулировке.
Теорема 7 — перестала быть теоремой
То, что было записано как доказательство, оказалось изложением наблюдения: величина ведёт себя так на всех проверенных случаях. Проверенных случаев было конечное число, и общего шага в рассуждении не было.
Переименована в «Наблюдение 7». Содержание не изменилось ни на слово — изменилась только этикетка, и это единственное, что было неверно.
Теорема 8 — дубликат Теоремы 2
Разные обозначения, разный путь доказательства, то же утверждение. Два доказательства одного факта — обычное дело и часто полезное. Дефектом была нумерация их как двух независимых результатов, отчего свод выглядел на один результат богаче, чем есть.
Что даёт ревизия
Ни одна из трёх правок не пришла извне. Все три видны при чтении собственного текста рядом с собственным доказательством — и ни одна не была видна при чтении заголовков.
Свод, который никто не перечитывал, не есть проверенный свод. Он есть список намерений, набранный шрифтом уверенности.
Устоявшие теперь стоят прочнее, чем восемь до ревизии: про каждую известно, что её читали с намерением сломать, и она не сломалась.
Чего это не решает
- Ревизия прошла 2026-08-11 по документу math-foundations/proofs.md; правки внесены на месте и датированы там же.
- Проверялись доказательства, а не численные подтверждения. Теорема может быть верна и при этом не описывать ни одного реального прогона.
- Восемь — это то, что было записано как теоремы. Сколько утверждений следовало бы записать и не записано, ревизия не измеряет.
- Дубликат найден по совпадению формулировок. Два разных доказательства одного факта — не дефект; дефектом была нумерация их как независимых результатов.
Пруфы
Поработаем вместе
Хотите так же проверить собственный дизайн?
Я аудирую RTL и строю независимые побитово точные модели, затем провожу результат через синтез и, когда это полезно, проверяю на плате Artix-7. Первый модуль проверки — бесплатно.