All of my public repositories are on GitHub at github.com/novaspivack. This post collects the non-Lean code projects — simulations, experiments, and mathematical software — along with pointers to the formal research they connect to.
For the Lean 4 formal proof libraries (17 repos covering the full NEMS research program), see the research index or the Zenodo program hub.
Simulations and Experiments
LACE — Link Automata Computing Engine
A new class of cellular automata in which both cell states and the links between cells are subject to the rules. Unlike Conway’s Game of Life and traditional CA, LACE rules can use neighborhood topology — the number and state of connections — as a first-class input. This enables a new family of emergent patterns: topological oscillators, gliders, and stable structures that have no analog in cells-only CA. Includes a GPU-accelerated mode via Taichi for large-scale simulations.
SocioLife — Socio-Economic Artificial Life Simulation
An agent-based artificial life simulation that runs in the browser. Agents evolve with genetic inheritance, form tribes, engage in trade (commercial bonds), diplomacy (diplomatic bonds), and war (war bonds). Includes a food chain, economic taxation, post-war reconstruction dynamics, and an alien-generated soundscape. Built in JavaScript; no install required.
Mathematical Software
Primes in Greedy B3
A proof and accompanying code showing that every prime number is admitted into the greedy multiplicative B3 Sidon set. The greedy B3 sequence is constructed by taking each positive integer in order if it does not create a multiplicative triple with any two already-chosen elements. This repository contains the formal argument and verification code.
neural-ca — Neural-Controller Cellular Automata
Two browser-based CA experiments in which a small neural network learns to tune the underlying rule parameters in real time, steering toward sustained complex behavior. Both run entirely in-browser with no install. The grid uses a hodgepodge-style update rule, but the parameter tuning layer — a tiny online-trained MLP paired with two cooperating RL agents (explorer + exploiter) — is original. One experiment adds trend-aware flee mode and 2-step lookahead; the other adds spatially varying parameter fields and a “greatest hits” snapshot memory that restores previously interesting states when the system gets stuck.
Experiment 1: Trend-Aware Agents ↗ · Experiment 2: Spatial Fields + Greatest Hits ↗
Lean 4 Formal Proof Libraries
The formal research program spans 17 Lean 4 repositories, each corresponding to a research area or paper cluster. All are machine-checked with a zero-sorry, zero-custom-axiom policy wherever achievable.
- nems-lean — No External Model Selection core library
- reflexive-closure-lean — Reflexive Closure, Alpha theorem, consciousness arc (Papers 53–70+)
- reflexive-reality-lean — Reflexive Reality umbrella library
- infinity-compression-lean — Certification exhaustion, Quillen homotopy data, fiber architecture
- representational-incompleteness-lean — Parametric self-model diagonal and topology
- aps-recursion-uniformization-lean — Abstract Programming Systems: separation theorem
- aps-rice-lean — Abstract formalization of Rice/halting for APS
- reflective-fold-obstruction-lean — Reachability and fold obstruction
- observer-non-exhaustability-lean — Observer classification and non-exhaustibility
- adequacy-architecture-lean — Outer admissibility and certificate worlds
- reflexive-architecture-lean — Strata synthesis (NEMS + APS + IC)
- reflexive-architecture-non-exhaustibility-lean — General science of reflexive systems
- phenomenology-lean — Phenomenology and consciousness formalization
- sentience-lean — Sentience and awareness formalization
- transputation-lean — Transputation and DSAC formalization
- novelty-theory-lean — Novelty Theory formalization
- ugp-lean — Universal Generative Principle formalization
- viable-continuation-lean — Viable Continuation formalization
Research Index and Archives
- Full research index — 93 papers, 17 Lean libraries, all programs
- Paper abstracts — all published abstracts in one navigable page
- Zenodo program hub — all papers and Lean archives archived with DOIs
- NEMS Corpus PDF Archive — all published papers as a single downloadable zip, numbered and indexed for AI-assisted reasoning
- novaspivack.github.io — source for the abstracts site