I have a new post on the Topos blog.

A topos can be specified by the geometric theory that it classifies. Though the sequents of a theory are described formally and syntactically, its interaction with the world of sets (through set-indexed disjunctions and axiom schemas) is often a little hand-wavy. In this post I describe two ways of doing this more precisely using type theory.

The values of the impartial game Officers are probably periodic eventually. Can we say anything about what the period could be?

(Previously, previously)

To not bury the lede, we finally have our first new value for the OEIS sequence A000769:

$$a(19) = 32577$$

This was calculated in 255 GPU-hours using eight RTX 4090s rented from Runpod.

Not only that! With help from Thomas Prellberg and the GPU cluster at Queen Mary University of London, we’ve been able to find some solutions with record-breaking sizes. The largest at the time I’m writing this is 64×64, shown below, with hopefully more on the way.

For the last month I’ve been completely addicted to the logic puzzle game Tametsi. Put briefly, it’s ordinary Minesweeper but with a set of 160 hand-crafted puzzles rather than a randomly generated starting board. Beyond the Minesweeper rules that we’re all familiar with, there are only a couple of additions: non-square/irregular grids for many of the puzzles, and “global” constraints, such as a fixed number of mines in cells of a particular colour or along a specified line.

I finally finished all the available puzzles and so Tametsi has released its grip on me. I’ve been trying to figure out what made it so compelling, and here’s the best I could come up with.

In the Game of Life, which still lifes can be produced by crashing gliders together? We’ve known for a few years that the answer cannot be “all of them”, because in 2022 Ilkka Törmä and Ville Salo found a patch of still life that, if it exists in the universe, must have existed since the beginning of time. And so, there is no way we could have produced it out of empty space through glider collisions. Similar such patches have been found since, with the goal of optimising size or population, and at the time of writing the record holder is an unsynthesizable still life with population 154 produced by forum user “400spartans”.

Finding syntheses for small still lifes is easy, but at some unknown point below 154 it becomes impossible. Today, we completed our collaborative project to notch the lower bound up from 22 to 23, by giving explicit syntheses for all 1,646,147 (strict) still lifes with population 23.