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

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.
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.
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.
LeanFrontier — open Lean 4 library of machine-generated, kernel-verified mathematics on Mathlib.
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.
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.

Agents, automation, and review workflows

topshift-trend — Telegram bot that watches new entries in GitHub monthly trending repositories.
caciarabot — Italian-first, self-hosted reactive Telegram group bot.
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

Ubuntu-Hardening — forked Ubuntu 24.04 CIS hardening script reference.
forgepulse — self-hosted GitHub traffic-history analytics: Rust, Svelte, SQLite, and Podman.
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.

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.