Skip to content
View Sanexxxx777's full-sized avatar
🏠
Working from home
🏠
Working from home
12 followers · 0 following

Achievements

Achievement: Starstruck

Achievements

Achievement: Starstruck

Block or report Sanexxxx777

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Sanexxxx777/README.md

Aleksandr Shulgin

Full-cycle engineer: bots, automation, websites, AI agents. I build systems that keep running without me.

Verifiable first: shulgin.is-a.dev/proof lists only links that open and can be checked in a minute.

Machine-checked mathematics

An agent pipeline that produces Lean 4 / Mathlib proofs, used to contribute to google-deepmind/formal-conjectures. Four PRs merged after maintainer review, every proof checked by the Lean kernel (#print axioms clean, no native_decide):

  • PR #4245: Erdos 1084, f1(n) = n - 1 for unit-distance configurations on a line (merged June 15, 2026)
  • PR #4244: Erdos 1052, the 24-digit unitary perfect number via a sigma-star multiplicativity API (merged June 22, 2026)
  • PR #4364: Green's open problem 64, the statement formalized with three witnesses of non-triviality (merged August 14, 2026)
  • PR #4361: Erdos 418, the Odd Noncototient Conjecture stated in Mathlib terms (merged September 2, 2026)

These are formalizations of known results and statements, not solutions of open problems.

Open source

Also

Unattended trading infrastructure (Python with a Rust hot path), 13 live UI mechanics with sources at shulgin.is-a.dev/lab, client websites, a free 152-FZ site check.

Site: shulgin.is-a.dev · Email: sanexxx777@gmail.com · Telegram: @Aleksandr_NFA

Open to remote roles (contract, part-time, full-time): AI/LLM engineering, Python backend, bots and automation. Business orders (websites, bots, integrations) are always open. GMT+10, async-friendly.

Pinned Loading

  1. erdos-openevolve erdos-openevolve Public

    Reproducing AlphaEvolve's SOTA bound on the Erdős minimum-overlap problem with an evolutionary LLM pipeline (OpenEvolve) — converges in ~10 iterations, two independent backends, one-command verifier

    Python

  2. server-hardening-playbook server-hardening-playbook Public

    Practical Linux server hardening — every item is failure → fix → verify. SSH, firewall, service binding, secrets, DB auth, and more.

    Shell 15 1

  3. curated-claude-code curated-claude-code Public

    A small, vetted, self-evolving harness for Claude Code — curated, not dumped. Skills, safety guards, and a self-improvement loop.

    16 1

  4. evidence-to-skill evidence-to-skill Public

    Turn untrusted source material into compact, attributed AI skills through evidence gates and deterministic safety checks.

    Python 11 1

  5. Ghostty-Agent-Face Ghostty-Agent-Face Public

    Living ASCII face on your Ghostty background showing AI agent status — thinking, done, needs-you. OSC 11 + GLSL shader, zero tokens, zero daemons.

    GLSL 1

  6. agent-graph-inspector agent-graph-inspector Public

    Turn a Claude Code Workflow run into one self-contained HTML page: every subagent a node, sized by real duration, with the timeline and critical path that set the wall-clock

    HTML