Linkage

The 3D Heesch Hemiobelisk: a nonzero-Dehn-invariant hexahedron with a complete corona (\(\mathbb{M}\)).

The Immerman–Szelepcsényi theorem formalized in Lean as part of the LAX Lean archive (\(\mathbb{M}\)), a form of literate programming for Lean proofs that includes definitions for computational complexity theory.

This year’s STOC call for papers has made significant changes, in the face of an onslaught of AI-generated submissions (\(\mathbb{M}\), via). Submissions must list authors, all of whom must be human, no author can be on more than five submissions, all submissions must be posted in identical form to arXiv prior to submission, AI use is allowed but must be disclosed, AI reviewing is also allowed subject to author consent, and (perhaps the biggest change) authors must also prepare and submit a 20-30 minute explanatory video.

Recognizing penny graphs is \(\exists\mathbb{R}\)-complete (\(\mathbb{M}\)), new preprint by Anna Lubiw and Marcus Schaefer. These are the graphs of tangencies of interior-disjoint unit circles, or equivalently the graphs with drawings that are simultaneously planar and unit-distance. They were known to be \(\mathsf{NP}\)-hard to recognize but this result makes their complexity more precise. The results extend to other geometric graph classes including the contact graphs of balls with unrestricted radii in 3d.

I’ve been using syncthing between home and office for a long time (\(\mathbb{M}\)). but somehow it hadn’t occurred to me that I could also use it to sync my music library between home computer and phone. Anyway, an up-to-date syncthing-fork is on Google Play and works for this. Unfortunately a long discussion on the syncthing forum fails to clarify how trustworthy it is.

Barrel game/puzzle (\(\mathbb{M}\)). Open and close pipes between given barrels of liquid to equalize their water levels, with the goal of getting at least a given level of water into one of the barrels.

The Cartesian product of two equilateral triangles is a 4d convex polytope with nine vertices and six triangular-prism facets, sometimes called the 3–3 duoprism (\(\mathbb{M}\)). Now remove one of the vertices and take the convex hull of the rest. You should get seven facets: an irregular tetrahedron where you removed the vertex, four pyramids (with a square base but unequal sides) surrounding it, and two triangular prisms that were unchanged by the removal. This heptatope has the property that no facet is adjacent (across a polygon) with all six others, because the facets all have four or five polygons, not six. It has the fewest facets of any convex 4-polytope with this property.

Cursed waffle (\(\mathbb{M}\)) with waffled indentations in the pattern of the tightest-known packing of 17 squares into a square.

Countable graphs with finite path-width: characterisation and universality (\(\mathbb{M}\)). New preprint by Tony Huynh, Freddie Illingworth, Nikolai Karol, Florian Lehner, Chun-Hung Liu, János Pach, and David R. Wood from a MATRIX workshop on graph structure theory.

How many L-seams does it take to sew Mrs. Perkins’s quilt (\(\mathbb{M}\))? New OEIS sequence from a practical crafting problem.

Abstract patterns from a hanging lamp and a dusty screen door (\(\mathbb{M}\)).

Talia Ringer worries about proof assistant kernel bugs in the Lean kernel, because although past bugs have not been things one might accidentally exploit and a human would have no incentive to do so, the rise of long unreadable machine-generated Lean proofs gives us a different threat model.

Discrete approximations to the Borel circle squaring problem generated by selecting a small set of translation vectors between a pixelated square and a pixelated circle and then solving a perfect matching problem. Solutions with five pieces can be found by using a heuristic search to find a good set of five translation vectors; it’s unclear whether fewer is possible.

NFC vs NFD unicode normalization (\(\mathbb{M}\)) or why you are probably encountering incompatibilities in filename encodings of accented characters between MacOS and everything else.

Hanayama makes massive versions of its most iconic cast puzzles (\(\mathbb{M}\)) and can ship internationally.