Александр ШульгинAleksandr Shulgin

google-deepmind/formal-conjectures · 6 PR приняты6 merged PRs

• #4245 Доказательство на Lean 4 для задачи Эрдёша 1084, принято в репозиторий Google DeepMind. A Lean 4 proof for Erdos problem 1084, merged into the Google DeepMind repository.
• #4244 Задача 1052: формальная привязка доказательства о 24-значном унитарно совершенном числе. Problem 1052: linking the 24-digit unitary-perfect proof through formal_proof.
• #4364 Открытая задача Грина №64: формализация вопроса о бесконечности нечётных значений. Green's open problem 64: formalizing the question about the infinitude of odd values.
• #4361 Эрдёш 418: формулировка гипотезы о нечётных нокототиентах, записана в Lean 4 в терминах Mathlib (постановка задачи, не доказательство). Erdos 418: the Odd Noncototient Conjecture stated in Lean 4 / Mathlib terms (a statement, not a proof).
• #6509 Эрдёш 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).
• #4379 Задача 90: формулировка в репозитории связана с внешним формальным опровержением на Lean (доказательство не моё), закрыт issue #4229. Problem 90: the repository statement linked to an external Lean disproof (the proof is not mine), closing issue #4229. внешнее доказательствоexternal proof

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

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

Сайты, сданы заказчикам, 2026Sites delivered to clients, 2026

• horsesfarm.ru Конюшня и контактная зооферма: страницы животных, услуги, события, галерея; владелец правит содержимое сам. A horse yard and petting farm: animal pages, services, events, gallery; the owner edits the content herself.
• tanyabunina.ru Сайт авторского курса по физиологичной расчистке копыт: программа из пятнадцати уроков, тарифы, видео, запись. A site for an author's course on physiological hoof trimming: a fifteen-lesson programme, tariffs, videos, sign-up.
• me4tut.ru Антикафе и клуб настольных игр в Санкт-Петербурге: залы под мероприятия с калькулятором аренды, посещение по минутам, коллекция игр в 3D-карусели. An anticafe and board-game club in Saint Petersburg: event rooms with a rental calculator, pay-per-minute visits, a 3D carousel of the game collection.

Сервисы, сданы заказчикамServices, delivered to clients

• Transaction Guardian Сервис мониторинга on-chain транзакций: подписка на события, фильтры по адресам и сигнатурам, алерты в Telegram, дашборд. A service for monitoring on-chain transactions: event subscriptions, filters by address and signature, Telegram alerts, a stats dashboard.
• Hub Research AI-ассистент крипто-ресёрча: собирает данные из множества источников, сводит в отчёты с LLM-аналитикой и отдаёт через бота. An AI assistant for crypto research: gathers data from many sources, distills it into reports with LLM analysis and delivers them through a bot.
• Twitter Intel Мониторинг X/Twitter по крипто-проектам с AI-саммари, скорингом важности и фильтром шума; алерты в Telegram. X/Twitter monitoring across crypto projects with AI summaries, importance scoring and noise filtering; Telegram alerts.