Открытый код

Публичная работа, которую можно проверить по ссылке: пул-реквесты, принятые чужими мейнтейнерами, рабочие программы и воспроизводимые результаты.

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

02 Принято в чужой код

google-deepmind/formal-conjectures #4245 merged ↗ Доказательство на Lean 4 для задачи Эрдёша 1084, принято в репозиторий Google DeepMind. google-deepmind/formal-conjectures #4244 merged ↗ Задача 1052: формальная привязка доказательства о 24-значном унитарно совершенном числе. google-deepmind/formal-conjectures #4364 merged ↗ Открытая задача Грина №64: формализация вопроса о бесконечности нечётных значений. google-deepmind/formal-conjectures #4361 merged ↗ Эрдёш 418: формулировка гипотезы о нечётных нокототиентах, записана в Lean 4 в терминах Mathlib (постановка задачи, не доказательство). google-deepmind/formal-conjectures #6509 merged ↗ Эрдёш 885, случай k = 4: доказательство на Lean 4 с явным свидетелем из компьютерного поиска (формализация результата Bremner, 2019). google-deepmind/formal-conjectures #4379 merged ↗ Задача 90: формулировка в репозитории связана с внешним формальным опровержением на Lean (доказательство не моё), закрыт issue #4229.

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

erdos-openevolve ↗ Эволюционный поиск, воспроизводящий известную числовую границу. В комплекте независимый проверяльщик: результат можно перепроверить одной командой, не веря на слово. erdos-computational-bounds ↗ SAT-поиск с сертификатами LRAT для трёх задач Эрдёша: доказательство проверяется машиной, а не читается глазами. transaction-guardian MIT ↗ Сторож транзакций для криптокошельков: разбирает, что именно подписывает пользователь, до подписи. pretrade-risk MIT ↗ Слой предторговых проверок для ордер-ботов: лимиты и запреты срабатывают до отправки ордера, а не после убытка. server-hardening-playbook MIT ↗ Скрипты первичной защиты сервера, написанные после разбора реального взлома, а не по чек-листу из интернета. agent-graph-inspector MIT ↗ Карта прогона многоагентной системы: видно, кто из агентов что сделал и где всё встало. pm2-cockpit MIT ↗ Аварийное управление процессами сервера прямо из Telegram, когда до ноутбука не дотянуться. fleetmap ↗ Список процессов превращается в самодостаточную HTML-карту флота: что где живёт и что из этого здорово. evidence-to-skill MIT ↗ Гейт, который не пускает непроверенный внешний материал в инструменты агента без доказательств. curated-claude-code MIT ↗ Методология и конвенции ежедневной работы через Claude Code: как устроен процесс, а не список ссылок.

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

Лаборатория приёмов ↗ Тридцать четыре интерфейсные механики, каждая работает в браузере. Не видео и не картинки: можно открыть и потрогать. horsesfarm.ru ↗ Конный двор в Сержантово. Хозяйка меняет тексты и фотографии сама, с телефона, программист для этого не нужен. me4tut.ru ↗ Антикафе и клуб настольных игр в Петербурге: залы, цены, бронирование. На сайт идёт реклама, он принимает гостей каждый день. tanyabunina.ru ↗ Страница авторского курса: программа, тарифы, запись. Живёт по своему адресу, автор ведёт её сама.

05 Как я меряю агентов

Перед выкладкой агентный конвейер прогоняется на фиксированном наборе задач, регресс виден до релиза. Прогоны трассируются: журнал каждого агента, критический путь и время по часам собираются в одну HTML-страницу (Agent Graph Inspector). На задачу считаются стоимость и латентность, у шагов с моделью есть фолбэк на другого провайдера, так работают Content Factory и агенты поиска работы. Что считается «сделано», описано лестницей доказательств в curated-claude-code.

Чего здесь нет и почему. Торговые системы, боты и клиентские проекты под соглашением о неразглашении в этот список не входят: показать их ссылкой нельзя, а верить на слово я не предлагаю. Про них — в разговоре, с цифрами и границами того, что можно рассказать.