ДоказательстваEvidence

Публичная работа, которую можно проверить по ссылке: пул-реквесты, принятые чужими мейнтейнерами, рабочие программы и воспроизводимые результаты. Public work you can check by link: pull requests merged by other maintainers, working software and reproducible results.

01 С чего начатьStart here

02 Принято в чужой кодMerged into other people's code

google-deepmind/formal-conjectures #4245 merged ↗ Доказательство на Lean 4 для задачи Эрдёша 1084, принято в репозиторий Google DeepMind. A Lean 4 proof for Erdos problem 1084, merged into the Google DeepMind repository. google-deepmind/formal-conjectures #4244 merged ↗ Задача 1052: формальная привязка доказательства о 24-значном унитарно совершенном числе. Problem 1052: linking the 24-digit unitary-perfect proof through formal_proof. google-deepmind/formal-conjectures #4364 merged ↗ Открытая задача Грина №64: формализация вопроса о бесконечности нечётных значений. Green's open problem 64: formalizing the question about the infinitude of odd values. google-deepmind/formal-conjectures #4361 merged ↗ Эрдёш 418: формулировка гипотезы о нечётных нокототиентах, записана в Lean 4 в терминах Mathlib (постановка задачи, не доказательство). Erdos 418: the Odd Noncototient Conjecture stated in Lean 4 / Mathlib terms (a statement, not a proof). google-deepmind/formal-conjectures #6509 merged ↗ Эрдёш 885, случай k = 4: доказательство на Lean 4 с явным свидетелем из компьютерного поиска (формализация результата Bremner, 2019). Erdos 885, the k = 4 case: a Lean 4 proof with an explicit witness from a computer search (a formalization of Bremner's 2019 result). google-deepmind/formal-conjectures #4379 merged ↗ Задача 90: формулировка в репозитории связана с внешним формальным опровержением на Lean (доказательство не моё), закрыт issue #4229. Problem 90: the repository statement linked to an external Lean disproof (the proof is not mine), closing issue #4229.

03 Открытый кодOpen source

erdos-openevolve ↗ Эволюционный поиск, воспроизводящий известную числовую границу. В комплекте независимый проверяльщик: результат можно перепроверить одной командой, не веря на слово. Evolutionary search that reproduces a known numerical bound. Ships with an independent verifier: one command re-checks the result instead of taking my word for it. erdos-computational-bounds ↗ SAT-поиск с сертификатами LRAT для трёх задач Эрдёша: доказательство проверяется машиной, а не читается глазами. SAT search with LRAT certificates for three Erdos problems: the proof is machine-checked, not eyeballed. transaction-guardian MIT ↗ Сторож транзакций для криптокошельков: разбирает, что именно подписывает пользователь, до подписи. A transaction guard for crypto wallets: it explains what the user is about to sign, before they sign it. pretrade-risk MIT ↗ Слой предторговых проверок для ордер-ботов: лимиты и запреты срабатывают до отправки ордера, а не после убытка. A pre-trade risk layer for order bots: limits and vetoes fire before the order goes out, not after the loss. server-hardening-playbook MIT ↗ Скрипты первичной защиты сервера, написанные после разбора реального взлома, а не по чек-листу из интернета. Server hardening scripts written after investigating a real break-in, not copied from a checklist. agent-graph-inspector MIT ↗ Карта прогона многоагентной системы: видно, кто из агентов что сделал и где всё встало. A map of a multi-agent run: which agent did what, and where the run stalled. pm2-cockpit MIT ↗ Аварийное управление процессами сервера прямо из Telegram, когда до ноутбука не дотянуться. Emergency process control for a server straight from Telegram, when a laptop is out of reach. fleetmap ↗ Список процессов превращается в самодостаточную HTML-карту флота: что где живёт и что из этого здорово. Turns a process list into a self-contained HTML map of the fleet: what runs where, and what is healthy. evidence-to-skill MIT ↗ Гейт, который не пускает непроверенный внешний материал в инструменты агента без доказательств. A gate that keeps unvetted external material out of an agent's tooling until it is backed by evidence. curated-claude-code MIT ↗ Методология и конвенции ежедневной работы через Claude Code: как устроен процесс, а не список ссылок. Methodology and conventions for daily work through Claude Code: how the process is built, not a link list.

04 Работает прямо сейчасRunning right now

Лаборатория приёмовInteraction lab ↗ Тридцать четыре интерфейсные механики, каждая работает в браузере. Не видео и не картинки: можно открыть и потрогать. Thirty-four interface mechanics, each running in the browser. Not videos or screenshots: open one and interact with it. horsesfarm.ru ↗ Конный двор в Сержантово. Хозяйка меняет тексты и фотографии сама, с телефона, программист для этого не нужен. A horse yard in Serzhantovo. The owner edits texts and photos herself, from her phone, with no developer involved. me4tut.ru ↗ Антикафе и клуб настольных игр в Петербурге: залы, цены, бронирование. На сайт идёт реклама, он принимает гостей каждый день. An anticafe and board-game club in St. Petersburg: rooms, prices, booking. It runs paid traffic and takes guests daily. tanyabunina.ru ↗ Страница авторского курса: программа, тарифы, запись. Живёт по своему адресу, автор ведёт её сама. An author's course page: curriculum, pricing, sign-up. Lives on its own domain and the author runs it herself.

05 Как я меряю агентовHow I measure agents

Перед выкладкой агентный конвейер прогоняется на фиксированном наборе задач, регресс виден до релиза. Прогоны трассируются: журнал каждого агента, критический путь и время по часам собираются в одну HTML-страницу (Agent Graph Inspector). На задачу считаются стоимость и латентность, у шагов с моделью есть фолбэк на другого провайдера, так работают Content Factory и агенты поиска работы. Что считается «сделано», описано лестницей доказательств в curated-claude-code. Before a release, an agent pipeline runs on a fixed set of tasks, so regressions show up before shipping. Runs are traced: every agent's journal, the critical path and wall-clock time are assembled into one HTML page (Agent Graph Inspector). Cost and latency are counted per task, and model steps have a fallback provider; Content Factory and the job-search agents work this way. What counts as "done" is described by the evidence ladder in curated-claude-code.

Чего здесь нет и почему. Торговые системы, боты и клиентские проекты под соглашением о неразглашении в этот список не входят: показать их ссылкой нельзя, а верить на слово я не предлагаю. Про них — в разговоре, с цифрами и границами того, что можно рассказать. What is missing and why. Trading systems, bots and NDA client work are not on this list: they cannot be shown as a link, and I am not asking anyone to take my word for it. Those come up in conversation, with numbers and clear limits on what can be told.