Projects

A curated map of public GitHub work. It favors active technical threads over a complete archive.

home.sh projects.sh blog.sh writing.sh cv.sh

Agents, automation, and review workflows

caciarabot — Italian-first, self-hosted reactive Telegram group bot.
topshift-trend — Telegram bot that watches new entries in GitHub monthly trending repositories.
llm-source-security-review — Codex skill and playbook for defensive source-code security reviews.
they-live-agent — local AR-style field-agent scanner experiment inspired by visual overlays.

Infrastructure, security, and operational tools

forgepulse — self-hosted GitHub traffic-history analytics: Rust, Svelte, SQLite, and Podman.
portcullis — two-phase hardened Ubuntu 26.04 VM provisioner for Hetzner Cloud: ~30-second lockdown first, then a full CIS-style hardening pass, verified by 58 checks.
Ubuntu-Hardening — forked Ubuntu 24.04 CIS hardening script reference.
pacenotch — Claude usage limits in the terminal, a tray icon and a window: a vertical notch on each bar marks where an even pace would leave you, so the fill says ahead-of-pace or room-to-spare at a glance.
cold-path-server-podman — run the Cold Path game server (jalhund/cold-path-server) in a Podman container.
dash — serverless DMARC aggregate-report parser for Gmail: extracts, parses, enriches failing sources, emails a summary.
sa-client-docker — SQL Anywhere client container setup with a Python connectivity test.
python-hosts-checker — AWS Lambda endpoint and certificate monitor with Telegram alerts.

Math, computation, and formal experiments

prove2me-logs — working log of Prove2Me formalization activity: per-mission entries with theorem uuids, Lean environments, and what remains open; a record of the work, not an archive of the proofs.
diaz-modulus-lean — Lean 4 formalization of a negative result on Diaz’s modulus conjecture: a candidate’s conjugate is a rational function of it, so no algebraic-hull matrix statement can separate it from an ordinary complex number.
sharp-symmetry-bounds-lean — Lean 4 formalization of sharp symmetry bounds for real plane algebraic curves: for an irreducible, non-circular real plane curve of degree d, the Euclidean symmetry group is finite, its rotation part cyclic of order at most max(d, 2d−4) and the full group of order at most 2d, with both bounds attained in every degree.
quadratula — how much of Le Floch’s implication semilattice of Schröder’s 990 quasigroup laws small quasigroups already witness: exhaustive enumeration to order 6, exact results to order 9, a provably optimal 17-quasigroup cover, and a generated report with independent checks.
magma-1518-obstruction-lean — Lean 4 on ETP law 1518: one-generated (1518+3862)-magmas are trivial or the Z/3 shift, and constant-coefficient magma cohomology cannot refute 1518 ⇒ 47/614/817/3862.
LeanFrontier — open Lean 4 library of machine-generated, kernel-verified mathematics on Mathlib.
unused-assumptions — Mathlib theorems whose stated typeclass setting is stronger than their proof needs; machine-found one-binder weakenings, each re-verified by the compiler at a pinned Mathlib revision.
unstated-conclusions — the dual of unused-assumptions: Mathlib theorems whose proofs establish a stronger conclusion than they state, read off the last step of the proof term.
parsimagma — magma signature and coverage engine over the Equational Theories Project law set.
dratify — in-process DRAT/DRUP unsatisfiability proof checker for Python and Rust: zero dependencies, with an optional Rust accelerator.
cdclkit — readable, self-checking CDCL SAT solver, preprocessor, and encoding library: every answer comes with a certificate (models re-checked, UNSAT backed by a DRAT proof an independent checker replays).
moebius-transcendental-lean — Lean 4 formalization of the conjugation degree on the transcendental locus (companion to p19), archived with a Zenodo DOI.
erdos-straus-offset-lean — Lean 4-verified fixed-divisor offset construction for 4/n = 1/x + 1/y + 1/z (not a proof of Erdős–Straus).
lean-corpus-density — dependency density in Lean 4 corpora, human and machine-generated, with evidence that machine mathematics accumulates. Reproducible from file headers.
inversive-geometry-lean — generalized circles (circlines) in Lean 4: circles and lines as one object, cut out by a Hermitian equation.
euclean — can a machine recover mathematical structure from an anonymized formal theory and a proof checker alone?
best-of-lean4 — curated list of awesome Lean 4 projects.
modular-zeta3-acceleration — SageMath pipeline for Apéry-type zeta(3) acceleration.
platosdf — genetic evolver for invariant signed-distance-field solids.
aristowrap — Docker-first CLI around Harmonic Aristotle, Lean 4, and Mathlib.

Visual and interactive systems

solids-hunter — first-person boolean-rule hunt: Babylon.js game with gamepad support and a shadow-pass watchdog.
cross-tetris — shared-queue 4-well cross variant of Tetris: Rust/WASM engine with a rule-based AI, played in the browser.
spriter — browser-only tool that turns a raster image into a pixel-art sprite. No upload, no build, no dependencies.
deck-lovers — Markdown-to-HTML deck with live audience likes and projector sync.
lifechess — chess-adjacent experiment mixing game structure and life-state modeling.
collective-canvas-3d — collaborative 3D painting app where phones act as brushes.
neon-bumper-cars — multiplayer WebSocket party game for live events.
agility-trainer — mobile-first bodyweight agility trainer.

Writing, philosophy, and structured notes

WIP articles and book PDFs — generated PDFs for the current book and standalone articles.