Optics have a very nice formulation used in some Haskell (and PureScript!) libraries; the so-called “profunctor representation”. Learners, defined a certain way, look an awful lot like some kind of two-sided or symmetric optic. Let’s see if we can devise a profunctor representation for them. This post was prompted by a chat with Bartosz Milewski.

There has been a lot of progress since my last update, catalogued on Achim Flammenkamp’s page. Most notably, Marijn Heule has come out of nowhere and smashed the size records using a new SAT solver; the record now stands at 76×76 (with four-fold rotational symmetry).

As for my GPU code, there hasn’t been any change there, just running it on larger systems for a longer time. One interesting result: the unique 47×47 solution with four-fold diagonal symmetry, displayed below. Thomas Prellberg has continued the search up to 57×57, but there hasn’t been another. Could this be the last in the symmetry class?

There’s a pattern I’ve seen more and more in political commentary, especially the Australian sources I pay attention to, where someone will make a sweeping diagnosis of a social problem in the language of things that we do wrong.

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?