Так думает среднестатистический пикабушник. Но моя статья не для всех, а именно для тех, кто хочет докопаться до истины. Бескомпромиссно и вычислительно точно. Так что заводчане проходят мимо!
Короче, к этой схеме я пришел просто потому, что устал. Знаете это чувство, когда спор заходит дальше пары абзацев? Сразу начинается каша: один понял так, другой эдак, третий вроде согласен, но с оговорками. И все, дальше аргументы кончились, начинается битва авторитетов и у кого глотка луженая. Никакой проверки, одна сплошная литература.
Я решил эту тему хакнуть. Упаковал всю теорию — аксиомы, правила, выводы — в один архив и заставил любую дискуссию проходить через жесткие фильтры, я их называю гейтами. Сменил подход с объясни мне на запусти это.
Теперь у любого утверждения есть ровно два состояния. Либо PASS — все работает, ничего не сломалось. Либо FAIL и предъявите witness — конкретный пример, который можно пощупать и на котором все валится.
ИИ — это всего лишь инструмент.
И тут начинается самое интересное, особенно если вы используете нейронки. Этот архив можно закинуть в абсолютно чистый чат, и сетка перестает галлюцинировать по памяти. Она начинает работать как бюрократ: смотрит в архив как в закон и проверяет все строго по пунктам.
Главный плюс — порог входа. Обычно, когда говорят про строгость, сразу представляются бородатые математики, которые пишут на Coq или Lean, или сутками сидят в матпакетах. Это круто, но для обычного человека это смерть.
Мой метод проще. Чтобы начать, не надо быть гуру алгоритмов. Делаем две вещи. Первое: описываем правила игры, хоть на русском, главное четко. Второе: пишем ИИ (тому же ChatGPT или Claude) промт вроде: Упакуй эту теорию в архив с гейтами. Все проверяем через PASS или FAIL с примером. Составь план прогонов и пиши отчеты.
Все. Дальше чисто инженерная работа. Правлю аксиомы, добавляю проверки, смотрю отчеты. И так по кругу.
Теперь про начинку. Чтобы эта штука работала как переносимая конституция, внутри должно лежать пять вещей. Аксиоматика — это база, что можно, что нельзя. Правила вывода — как из А получаем Б. Гейты — сами проверки, да или нет. План прогонов — чтобы не забыть проверить главное. И отчеты — чтобы видеть историю болезни. В итоге теория перестает быть просто текстом, который можно переврать, и становится исполняемым файлом.
Самая киллер-фича — это работа с новым контекстом. Все знают: в длинном чате ИИ вроде умный, а начнешь новый — он чист как лист. А через пару дней опять начинает плыть в терминах. Архивный режим это лечит. Я беру архив, кидаю в новый чат и сразу ставлю условие: Источник истины — только этот архив. Любое утверждение — через гейты. Ошибка — только с пруфами.
После этого ИИ превращается из болтливого собеседника в скучного оператора. Он читает доки, запускает тесты, предлагает правки и тут же их проверяет. Закон теории переезжает вместе с файлом, а не держится на честном слове.
Работа идет итерациями. Добавил аксиому — прогнал тест. Уточнил правило — прогнал тест. Получил отчет: где PASS, где FAIL. Контрпример — это вообще лучшее, что может случиться. Это конец спора в стиле я художник, я так вижу. Если пример воспроизводится — значит, теория дырявая. И мы не спорим, кто дурак, а правим баг.
Чтобы не быть голословным, сравню с тем, чем пользуются профи.
Доказательные ассистенты типа Lean или Coq. Порог входа — космос. Надежность железобетонная, но менять аксиомы — адски долго.
Логические решатели SMT, типа Z3. Надежно, но все надо кодировать в логику, шаг влево-вправо — расстрел.
Поиск контрмоделей, Mace4. Удобно для малых задач, но язык бедный.
Матпакеты типа Mathematica. Порог низкий, но это просто мощный калькулятор. Он считает, а не доказывает. Если не задать рамки, контекст уплывет.
Вычислительная алгебра, GAP. Круто, но ограничено встроенными моделями.
Физические симуляции. Надежно, пока настройки не трогаешь. Но формальной истины там нет, все на допущениях в коде.
Я не пытаюсь их заменить. Я добавляю то, чего вечно не хватает в спорах: единый формат ответа PASS/FAIL и протокол как документ.
Для алгебраиста это родная среда. Для физика тоже, просто оформленная иначе. А для остальных кайф в том, что не надо разворачивать сервера. Упаковал теорию в текст, скормил ИИ, и гоняешь итерации.
Я считаю, этот метод может перевернуть игру. Не потому что он самый строгий, а потому что делает строгость дешевой. Если подход теория как архив станет стандартом, мы наконец перестанем спорить о словах. Спор будет упираться в кнопку Запуск. И архив можно пересылать кому угодно, закон теории останется неизменным.
И, наконец, вспомните, про Интернет в 90-х, еще до бума доткомов, когда все было также не так очевидно.
P.S. Про хронологию: почему я сначала топил за граф, а потом передумал.
Раньше я топил за то, что мировую хронологию надо собирать как граф событий. Узлы, связи, кто на кого повлиял. Это красиво и удобно для навигации. Но потом до меня дошло: граф сам по себе не делает утверждения истинными. Он просто хранит структуру. В нем легко накопить красоту, но трудно добиться строгости.
Во-первых, нет обязательного свидетеля при конфликте. Если даты не бьются, граф это просто покажет, но не ткнет носом в причину.
Во-вторых, критерий параллелей плавает. На картинке все кажется похожим, а мне нужен четкий ответ: да или нет.
В-третьих, с календарями там черт ногу сломит, и граф не заставляет доказывать, что конверсии верны.
И главное: гипотезы о сдвигах времени в графе превращаются в болтологию. Типа, если сдвинуть на сто лет, вроде похоже... А мне нужен инженерный режим: задал сдвиг, прогнал тесты, получил PASS или FAIL с точными местами, где история сломалась.
Поэтому я переобулся. Граф — это отличная картинка, интерфейс. Но фундаментом должен быть архив. События, источники, версии — все через гейты. Любая гипотеза — только через прогоны. А граф пусть остается сверху для красоты. Истина живет не в картинке, а в контрпримерах.
Так что держитесь, сынки, я поменял правила игры.
Замечание: это работает лишь в ChatGPT Plus / Claude Pro. Примеры архивов Вы можете найти у меня в статьях (байт на чтение моих статей).
Подписывайтесь, кто хочет увидеть продолжение этой галиматьи. Следующая статья будет посвящена ИИ нового типа, который будет упакован вместе с теорией в презентабельном для Бигтеха виде в подобный архив. Вы будете свидетелями новой эпохи.
[1] The mathlib Community. The Lean Mathematical Library. arXiv:1910.09336, 2019. (Springer Nature)
[2] The Coq Development Team. The Coq Proof Assistant, software record. Zenodo, 2023.
[3] de Moura L., Bjørner N. Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963. Springer, 2008.
[4] Barbosa H. et al. cvc5: A Versatile and Industrial-Strength SMT Solver. In: TACAS 2022. Springer, 2022.
[5] McCune W. Mace4 Reference Manual and Guide. Technical Report, Argonne National Laboratory, 2003.
[6] Jackson D. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 11(2), 2002.
[7] Wolfram Research, Inc. Mathematica, Version 14.3. Champaign, IL, 2025.
[8] The Sage Developers. SageMath, the Sage Mathematics Software System.
[9] The GAP Group. GAP — Groups, Algorithms, and Programming.
[10] Bosma W., Cannon J., Playoust C. The Magma Algebra System I: The User Language. Journal of Symbolic Computation, 24(3–4), 1997.
[11] Agostinelli S. et al. Geant4—a simulation toolkit. Nuclear Instruments and Methods in Physics Research A, 506(3), 2003.
[12] Brun R., Rademakers F. ROOT — An object oriented data analysis framework. Nuclear Instruments and Methods in Physics Research A, 389(1–2), 1997.
[13] Alwall J. et al. The automated computation of tree-level and next-to-leading order differential cross sections. Journal of High Energy Physics, 2014.
[14] Johansson J. R., Nation P. D., Nori F. QuTiP 2: A Python framework for the dynamics of open quantum systems. Computer Physics Communications, 184(4), 2013.