Tavis Rudd

@www.stephendiehl.com I built something which might interest you github.com/tavisrudd/co... a specialized CP-SAT-style solver that exploits compositional algebra to compile huge search spaces into small exact dynamic programs. Saw your old OR-tools post while building it.

28 Aug

yikes, bsky is crap with svg images.

My new paper on a geometry problem open since the 1970s: can a cubic threefold (a 3D geometric object defined by a cubic equation) become "simple" if you give it an extra dimension? No. Even after adding that extra dimension, its underlying algebraic complexity stubbornly survives.

This was a lot of work with many false starts. I finally got to use the fancy category theory I learned through Haskell for some real math. It hasn't been fully peer reviewed yet but I'm finally confident enough to not doubt it. #math

Repo github.com/tavisrudd/cu... The lean formalized proof is in github.com/tavisrudd/cu... along with proofs for its companion papers. Each manuscript claim has detailed verification metadata and the paper's LaTeX is marked up for rendering with leanblueprint

@www.stephendiehl.com finally been putting my new lean skills to good use

Since Sol and Fable came out I've been obsessively using them for research math and putting my Lean skills to use. The result is a series of thematically connected papers in algebraic and finite geometry, coding theory, algebraic combinatorics, and quantum information. github.com/tavisrudd/ma...

... My naive questions and challenges seemed to help the models push past their natural stopping points and not cheat. /goal is dangerous for this type of work and I've avoided it.

I've reached out to a bunch of specialists whose work I've cited and extended and expect at least part of this to be classical work rediscovered or just wrong in various ways. I hope what survives is interesting.

They ask two related questions: how much structure can be recovered after most of the original information has been discarded, and which obstructions persist under operations, such as stabilization, that might be expected to weaken them?

This was not zero-shot! I've been in the loop over 1,552 codex and claude code sessions choosing and reframing problems, steering exploration and later proof & manuscript development, challenging arguments, and designing verification gates. ...

1 July

Fable in its first 200K tokens shattered the record Opus and I had been stuck at for days on Non-Attacking Queens 16x16 solves. -38% wall time, -37.6 % nodes. 14.6 seconds. It moved like a killer. bsky.app/profile/tavi...

Tavis Rudd@tavis.damnsimple.com

I've been obsessed with coding fast adversarial game tree solvers this week. Warmed up on Othello and then wrote dozens of increasingly fast solvers for Non-Attacking Queens. Record 16x16 in 24sec. This needs to be verified but here is the first ever 18x18 board solve.

2 July

Fable landed at 12.43s / 176M nodes. 270x faster than my original and half the time of its already heavily optimized starting point.

The solvers are "exact" unlike chess or go solvers which can't possibly be.

27 June

n=18 result is legit. verified via: • 2 independent solvers: same verdict, same move (I9), byte-identical 15-move PV • Lean-checked game recurrence • oracle differential, 3,400 subpositions • reproduces known n≤16 results (Jenrich) • rules-only certifier, zero solver code

Since Claude Code and Codex came out all my hobbies have been geeky versions of "Faster, Better, Stronger". I need to step away from this addiction and get back to making my body that. bsky.app/profile/tavi... bsky.app/profile/tavi... bsky.app/profile/tavi...

Tavis Rudd@tavis.damnsimple.com

The final used Normal-play minimax with ab pruning Node Kayles reduction D₄ group actions Canonicalization Graph isomorphism Dynamic programming Transposition DAGs Dense endgame tables Bitset set algebra Cutoff-rank statistics And a bunch of asm micro optimized kernels for various hotspots

Consumer hardware: 12 core (24 hardware threads), 26GB ram, ryzen 5. Geekom A9 Max. Rust code leveraging all the hardware optimizations it can, following "Tiger Style" perf rules. DRAM latency on the Transposition Table is the limiter not core count or speed. Faster memory would improve it further

My 1st solver was a parallel depth first search using D4 symmetry fold, Transposition Table, minimax + alpha-beta pruning, and Younger Brothers Wait parallelism.

In English: boards into occlusion maps; folded rotations/reflections; cache repeated positions; packed into tiny cache entries; pre-solved small endgames; CPU bit tricks; tried most-forcing moves first; cache check before search; parallelized roots; tuned with detailed search telemetry.

loses.jstor.orgloses.jstor.org

This isn’t the classic n-queens puzzle. It’s a two-player game: players alternate placing queens so none attack; each move blocks its row, column, and diagonals; the player with no legal square left loses.jstor.org/stable/27646335 PSPACE-complete complexity vs NP or #P for n-queen

The charts above are absolute and relative scale progress on wall time, search node count, and ns/node. The algorithmic improvements in node pruning dominate.

13 June

In the month since I posted this latency chart for my search engine project bsky.app/profile/tavi... I've managed to eek out another 57x speedup on the p99 -> 12µs. 450x faster than the original chart.

Tavis Rudd@tavis.damnsimple.com

Been going "tiger style" with perf optimizations. 10x speedup between first image and second/third. Now p50@ 26µs p95@ 271µs p99@ 695µs :)

Been going "tiger style" with perf optimizations. 10x speedup between first image and second/third. Now p50@ 26µs p95@ 271µs p99@ 695µs :)

3 June

This is about as far as I can take it. One run with all caches/speculation on, another with them all off

medium.comrsync and outrageI gave up blogging a long time ago (apart from an occasional thing about ArduPilot), I tend to just write code and hope people find it…

9 June

Managed to shave another 110 off the p99 with all caches off. P50 36µs, p95 83µs, p99 117µs.

Tavis Rudd reposted

Armin Ronacher

@mitsuhiko.at

3 June

In case you are in the camp of “Andrew Tridgell is vibefucking rsync” please read this.l and adjust your priors. medium.com/@tridge60/rs...

Been going "tiger style" with perf optimizations. 10x speedup between first image and second/third. Now p50@ 26µs p95@ 271µs p99@ 695µs :)

28 May

Another level up: p99 139µs. Aiming for sub 100

1 June

To the max now with vastly improved speculative prediction of the queries as you type. P99 = 41µs

Been going "tiger style" with perf optimizations. 10x speedup between first image and second/third. Now p50@ 26µs p95@ 271µs p99@ 695µs :)

PGO build: 22µs p50, 253µs p95, 615µs p99, 1.1ms max from keystroke to first-page results

27 May

p50 18µs, p99 242µs

michaelgeist.caThe Lawful Access Two-Headed Surveillance Monster: How Bill C-22 Went Off the Rails - Michael GeistThe government’s plans for lawful access have gone off the rails. In recent days, Signal has warned it would pull out of the Canadian market rather than comply with Bill C-22. Windscribe, the Toronto-...

@mark-carney.bsky.social please ensure C-22 goes back to the drawing board. This is not ok www.michaelgeist.ca/2026/05/the-...

6 May

Having fun making my new incremental search tool very fast p75 @ 82μs, p95 @ 515μs

Noisy teenage ravens in the park

@carlbergstrom.com have you seen www.imdb.com/title/tt2642...? It's on Prime Video atm (appropriately directed by Vance *Crofoot*)

imdb.comimdb.com

24 Mar

4 Mar

4 Mar

2 Mar

@shriram.bsky.social your "ghost" wrote a review github.com/tavisrudd/ii.... Feel on point?