About
I am a sixth-form student in the United Kingdom, working on exact values in Ramsey-type combinatorics and on software built around a single idea: a result is worth what its verification is worth. Where a claim can be made checkable by someone who does not trust me, I make it checkable.
- 174 accepted OEIS terms across 21 sequences
- 23,851 per-cube DRAT proofs, every one replayed by drat-trim
- 5 new mixed van der Waerden numbers, in sequences unmoved since 2012
OEIS figure re-derived from the live database on 2 September 2026 by a script that fails if the number has moved, rather than typed from memory.
News
- 2 Sep 2026
- A337114 published: a(25) to a(36), twelve terms appended beneath the previous author's last value. The total is now 174 accepted terms across 21 sequences.
- 1 Sep 2026
- All five upper bounds are now machine-checked. The equal-target families had resisted: the cube generator dropped colour-permutation images, which is sound for searching but is not a refutation, so the per-cube proofs never covered those branches. Taking colour symmetry out of the cube set closed it, and the total stands at 23,851 per-cube DRAT proofs across the five families.
- Three more sequences published — A325556, A347414 and A353403. That takes the total to 162 accepted terms across 20 sequences.
- 31 Aug 2026
- Seventy-one terms approved in one day across A319381, A323586 and A325555 — sequences whose published range had stopped where a brute force ran out of patience.
- Aug 2026
- Five new mixed van der Waerden numbers, with machine-checked upper bounds is being prepared for submission to Experimental Mathematics.
- 4 Aug 2026
- The headline upper bound stopped resting on a solver's word: w(14; 212, 3, 4) = 57 reduced to 4,487 per-cube DRAT proofs, all replayed to s VERIFIED, with a checked proof that the cube set is exhaustive.
Research
My main line is mixed van der Waerden numbers w(j+r; 2j, t1…tr) — families whose OEIS entries had stood unchanged since Tanbir Ahmed's work in 2012. Each new term needs two independent halves, and they are not equally trustworthy:
- The lower bound is a certificate. A colouring of [1,n] with the required property. You read the string, apply the definition, and you are done — no solver, and no trust in me.
- The upper bound asserts that no colouring exists. That is only as good as the SAT encoding behind it, so it is the half where the real work sits, and where I say so plainly.
Check it yourself
You should not take the figure above on trust, and you do not have to. This reads the colouring back out of the page you are looking at and re-derives the property from the definition — it enumerates the arithmetic progressions itself rather than comparing the page against a second copy of my answer. No dependencies, standard library only, about a second to run:
git clone https://github.com/Leo-Y-Zhang/PersonalWebsite
python PersonalWebsite/tools/verify_certificate.pyIt prints the two classes it found, confirms every position in [1,56] is coloured exactly once, and exits non-zero if the page is wrong. If I ever edit the figure and break the claim, this fails in continuous integration before you see it.
Research interests
The directions I want to work in, and where each one currently stands for me. I have listed what exists rather than what I intend, so the difference between the two is visible.
-
Exact values in Ramsey-type combinatorics
Van der Waerden and related numbers, where the object of study is a single integer nobody knows. The appeal is that progress is unambiguous: a bound either holds or it does not.
Five new terms computed; all five published by the OEIS, the last approved 13 August 2026.
-
SAT encodings and proof certificates
An unsatisfiability result is a mathematical claim resting entirely on an encoding. I am interested in the gap between "the solver said UNSAT" and "this has been proved" — DRAT-style proof objects, independent checkers, and symmetry breaking that is justified rather than assumed.
Upper bounds reduced to machine-checked proof objects where stated; where not, said so.
-
Counting on structured graphs
Independence, domination and connected domination on board graphs. A change of coordinates can collapse an exponential count into a frontier dynamic program — the bishop graph is a rook graph rotated, which turns O(2n²/2) into a DP over O(n) classes per side.
Fourteen new terms across seven sequences, all published by the OEIS, the last on 15 August 2026.
-
Verification of algorithms, not just of code
Deterministic simulation testing, machine-checked invariants, and exact equivalence rather than sampled agreement: safety properties checked after every step, compiler passes proved by unitary equivalence, gradients checked against finite differences.
The recurring design constraint across everything below.
-
Honest inference from small samples
Most quantitative claims fail statistically rather than logically. I am interested in default-deny methodology: finite-sample bounds, multiple-testing corrections, and reporting that refuses when the evidence does not reach the bar, instead of reporting a number anyway.
Applied to benchmark scores, quantum measurement claims, and backtested track records.
Contributions to the OEIS
| Sequence | Term | Value | Status |
|---|---|---|---|
| A217058 | a(12) | 57 | published — credited 30 July 2026 |
| A217005 | a(19) | 52 | published — credited 7 August 2026 |
| A217007 | a(7) | 68 | published — credited 7 August 2026 |
| A217236 | a(4) | 84 | published — credited 7 August 2026 |
| A217059 | a(9) | 74 | published — credited 13 August 2026 |
Board graphs, same discipline. The counting line has landed in full: ten further terms across A290719, A290769 and A291595 (connected induced subgraphs of the black, white and full bishop graphs) and A289145 and A289169 (connected dominating sets), all published on 13 August 2026. An eleventh, A290783 a(10), carries the same count onto the triangular honeycomb bishop graph, where the previous term had stood since 2017; published 14 August 2026. Three more, A381795 a(8)–a(10), count the connected dominating sets of that same honeycomb graph, an entry that had stood at seven terms since March 2025; published 15 August 2026.
Thirty-two further terms, same standard of evidence. A250026 a(31)–a(60), thirty terms beginning a(31) = 41, the 2-colour Rado numbers for x12+…+xn2 = z2, and A398541 a(16) = 241 and a(17) = 274, the least k forcing an n-term arithmetic progression whose signed sum is at least 2 in absolute value; published between 13 and 30 August 2026.
Sequences a brute force had abandoned. A survey of the OEIS for entries whose published range stops where an exhaustive search ran out of patience rather than where the mathematics gets hard, followed by exact enumeration past them: A319381 a(23)–a(50) (plane trees), A323586 a(14)–a(40) (plane partitions with no repeated rows) and A325555 a(26)–a(41) (necklace compositions with distinct circular differences) — seventy-one terms, all approved on 31 August 2026. Each is gated on a program that first reproduces every already-published term of its sequence, so exact agreement across the known range is what makes the new range worth reading. One hundred and seventy-four accepted terms across twenty-one sequences in total.
Paper
Five new mixed van der Waerden numbers, with machine-checked upper bounds. Being prepared for submission to Experimental Mathematics. [paper] [code and certificates]
Method, encoding, the certificates, and an explicit account of which claims rest on which kind of evidence. The distinction the paper is careful about, because it is the one a reader would otherwise get wrong:
- Every upper bound is a proof object. All five are reduced to per-cube DRAT proofs — 23,851 in total, each replayed to s VERIFIED by drat-trim against a single formula hash — and each family carries a separately checked composition proof that its cube set covers the whole assignment tree.
- The equal-target families were the hard ones. The cube generator dropped colour-permutation images, which is sound when you are searching, because some other prefix is the image, but it is not a refutation, so the per-cube proofs never covered those branches and [3,3] and [4,4] could not be certified at all. Taking colour symmetry out of the cube set fixes it, and the effect is measured rather than argued: the cube sets are byte-identical with and without it for the differing-target families, and exactly double for the equal-target ones.
Across all five families the certification run produced 23,851 per-cube proofs. The tooling, computation and drafting involved substantial AI assistance, disclosed plainly in the paper's Methods section; the verification programme exists so that a reader does not have to take that on trust.
Software
Each of these exists to make a claim checkable rather than to assert it. The full portfolio — production software, team projects, and everything else — has its own page.
- MathRecords Python
- The van der Waerden work: search, SAT encodings, and a certificate for every lower bound.
- GradForge Python
- A reverse-mode autograd engine and a small GPT on top of it, 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.
- Splitbrain Go
- Drives a real key-value cluster through seeded TCP partitions and machine-checks whether what the clients observed was linearizable; the checker is validated against a brute-force oracle.
- Osmium Rust
- An x86_64 operating system from scratch that boots on BIOS and UEFI and preemptively schedules ring-3 user programs, each in its own address space — a crashing program is terminated alone and the machine keeps running — with a shell and a RAM-only filesystem; a CI boot test proves its privacy claims — no network stack exists, freed memory is zeroed, and nothing reaches the disk.
- 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 Shapley attribution.
- 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.
Contact
Everything I publish is at github.com/Leo-Y-Zhang. For anything about the van der Waerden work you can write to me at academic.submissions26@gmail.com, or open an issue on MathRecords, which keeps the discussion next to the certificates it concerns.