RRBBRRBB: the colouring of 1 to 8 that shows W(3,3) > 8

Leo Y. Zhang

Projects — the complete portfolio

Sixth-form student, United Kingdom

At a glance

48 public repositories, with continuous integration on 47 of them · 174 accepted OEIS terms across 21 sequences · one live production web application · over 3,700 automated tests measured across the two flagship systems. Repository figures re-derived from the live sources on 6 October 2026 and the OEIS figure on 2 September 2026; the test counts were measured on 26 August 2026. The research itself is on the home page, with the certificate to prove it.

Flagships

MathRecords Python
The published combinatorics: SAT encodings, DRAT proof certificates, and a verification gate (verify_all.py, in CI) that re-derives every published value from scratch before it is quoted — the five new mixed van der Waerden values ride on it. The full story is on the home page.
Osmium Rust
An x86_64 operating system from scratch, closed at v0.6.0: BIOS and UEFI boot, preemptive scheduling of ring-3 programs in isolated address spaces — a crashing program dies alone — a shell, and a RAM-only filesystem. A CI boot test proves the privacy claims: no network stack exists, freed memory is zeroed, nothing reaches the disk.
Tilefish C++
A championship-style Scrabble engine in one C++ file using only the standard library: move generation, Monte Carlo simulation, endgame solving and self-play training, with every shortcut checked against brute force. Its strength is measured, not asserted: logged matches under a neutral referee against the strongest public engines, MAGPIE and Macondo, with the opponents pinned to recorded versions and the results and their limits in the repository. Play it in the browser.
Production web application TypeScript · PostgreSQL · private
A live product with real users, designed, built, deployed and maintained solo: row-level security, versioned migrations, staged deployments behind a manual production gate, and roughly 980 unit plus 85 end-to-end browser tests. The repository is private because it holds operational configuration, and the product is not named here; details on request.
Systematic trading research platform Python · private
Institutional-grade engineering around an honest research core: an immutable hash-chained event ledger, broker reconciliation with operator-gated resolution, a latched kill-switch battery, a supervised paper-trading deployment, and a browser operations terminal — 3,574 automated tests measured 26 August 2026, with mutation testing on the safety-critical seams. Every candidate strategy faces deflated-Sharpe and overfitting gates that default to rejection, and most fail: results are pre-registered before they run, and the status document is generated from the system, never typed.
ClimateMesh Python · Raspberry Pi
Decentralised climate early-warning, built as the software lead of a two-person team: twenty sensing nodes scoring flood and heat risk 0–100 in real time on one Raspberry Pi, an explainable anomaly model, and honest data-source provenance — a reading is labelled hardware only when a physical sensor produced it. 236 automated tests (6 October 2026) and a one-command judge validation passing 5/5 (26 August 2026).

Team & competitions

EndeavourRacing TypeScript
The team's three web applications for STEM Racing 2026: public site, lap-timing and driver-performance tool, and a project, risk and budget dashboard.
Wharton Global High School Investment Competition 2026–27
Entered as part of a team; the trading round runs September to December 2026.
Independent research manuscript June 2026
Sixty-two pages on network structure in equity markets: the framework is validated on synthetic data, and the empirical validation is specified but deliberately not yet claimed.

Everything else, one line each

Each of these exists to make a claim checkable rather than to assert it.

HartBeat Rust
An RV32IM RISC-V interpreter, tested against the architecture's official compliance vectors rather than hand-written cases.
Ratified Lean 4
A machine-checked proof-checker development: the soundness argument lives in a proof assistant, not a comment.
Splitbrain Go
Partition-tests a real key-value cluster and machine-checks the observed histories for linearizability; the checker is validated against a brute-force oracle.
GraphRecords Python
The frontier dynamic programs behind the board-graph OEIS terms — exact counts where brute force is O(2n²/2).
BishopVerify Python
An independent verifier for those counts — the published numbers are re-derived by different code before they are trusted.
CipherTool Python
A classical-cipher solver run on forty published National Cipher Challenge ciphertexts: all twenty-two with a published answer solved, the other eighteen recorded as unverified rather than solved, and none labelled strong while wrong.
GradForge Python
A reverse-mode autograd engine and a small GPT on top, from scratch; every gradient is checked against finite differences.
PathTracer TypeScript
A deterministic Monte Carlo path tracer whose 278 tests validate the rendering physics, not just the code.
DeterministicRaft Python
Raft consensus under a seeded fault simulator; the five safety properties are checked after every step and any failure replays from its seed.
QuantumCompiler Python
A teaching quantum-circuit compiler whose optimisations and SWAP routing are proved correct by exact unitary equivalence.
QuantumClaimReferee Python
A finite-sample referee for quantum measurement claims: memory-robust CHSH p-values and default-deny verdicts.
EvalAssay Python
Splits a reported LLM benchmark score into measured capability and measured artifact, with exact Shapley attribution.
ProjectSentinel Python
A pitch-book generator where no figure is typed by hand: a CI gate checks every tagged figure against a tested model and fails if it finds nothing to check. The content is deliberately fictional; the pattern is the product.
Understudy TypeScript
An AI interview simulator, v1 live.
ChessPuzzleForge Python
An offline mate-in-N generator; a bundled from-scratch engine re-proves every puzzle before it is emitted.
TerminalAgent TypeScript
A terminal coding assistant with per-turn checkpoints and an /undo that refuses when it cannot restore.
Refute Rust
An independent DRAT and LRAT proof checker with no dependencies, and a browser playground where proof files never leave the tab.
MeltSim TypeScript
Melting, freezing and boiling from one enthalpy conservation law, benchmarked against the analytic Stefan solution; runs in the browser.
VisionCheckR JavaScript
A privacy-first vision self-check that runs entirely in the browser; nothing is uploaded. Not a medical device.
RadoRecords Python
2-colour Rado numbers for x12+…+xn2 = z2, carried from a(30) to a(60) with DRAT-certified refutations.
OEISHeadroom Python
Finds OEIS sequences that stopped where a brute force ran out of patience, then extends them, each gated on reproducing every published term first.
DiscrepancyRecords Python
A SAT campaign on Erdős problem #176 (OEIS A398541), with a cold verification gate that must pass before anything is claimed.
CycleRamsey Python
Three-colour cycle Ramsey numbers as SAT, with a measured account of how far one desktop machine gets.
PalindromicVDW Python
Palindromic mixed van der Waerden numbers as SAT, with the same measured account of its limits.
IaCScanner Python
A read-only, offline infrastructure-as-code scanner for Terraform, Kubernetes, Actions and Dockerfiles, with SARIF output.
DocRedact Python
A local-first document redaction CLI: validator-driven detection, consistent tokens, and no network access.
SuiteAudit Python
Finds the tests that cannot fail: tests that would stay green whatever the code did.
FireTurret Python
A camera-guided fire-suppression turret demonstrator that corrects its aim by watching where the water lands; simulation only, with the safety case written down.
TradingEngineResearch Python
The research core of a systematic trading platform: a pre-registered alpha search across five data sources whose honest result was negative.
FilingsLab Python · TypeScript
Backtests the disclosure delay in political and insider trades, trading only once a filing is public.
BacktestAudit Python
Reports how much of a backtest's apparent edge survives luck, non-normal returns and multiple testing.
HawkesDiffusion Python
Cross-exciting Hawkes processes fitted to market event streams, with the identification failures reported rather than hidden.
ImpliedDensity Python
Risk-neutral densities from option prices via Breeden–Litzenberger, and where the method breaks.
PredictionArbitrage Python
Arbitrage detection in prediction markets, every reported number rendered from the results file.
FinanceEngine Python
A UK personal-finance answer engine that answers only with a named, dated citation, and otherwise says so.
GreekScansion Python
Scans Greek dactylic hexameter and reports only what the metre itself settles.
LiberPrimusAnalysis Python
Cryptanalysis of the unsolved pages of Cicada 3301’s Liber Primus: not solved, but a reproducible toolkit and an exclusion ledger.
BoundarySeverance Python
A geometric permutation test for whether a political boundary bends a city’s road network.
InformaticsOlympiad2025 Python
British Informatics Olympiad 2025 Round One solutions, with brute-force checkers for the written answers.
ChessEditForge JavaScript
Renders vertical chess videos to MP4 entirely on the local machine, with no external assets.
MacBookHomelab Docker · Shell
A 2015 MacBook Air turned into a modular home server: one Compose file per service, reachable only over Tailscale.

Method

The through-line: claims are cheap, verification is the work.