Week of the 10/5/2026 - #41

Contents

science

• AI Mathematics progress

tech

• Build a $40 WiFi e-reader
• More DIY audio projects
• Watt: the lean desktop project
• Sega Genesis trackers

art

• Poster prompts
• Encyclopædia Britannica

AI Mathematics progress

Over the past couple of months, there have been interesting developments in using AI to prove mathematical theorems. Most notably, there were two major events. In September 2026, OpenAI announced a proposed proof for the Navier-Stokes existence and smoothness problem. Although it has not yet been officially verified by the broader mathematics community or accepted by the Clay Mathematics Institute, the result is still interesting. There are, of course, controversies and issues with the proof, but it is nonetheless an interesting application. The second event happened this week, when OpenAI released a GitHub repository with more than 370 articles proving mathematical propositions from almost every field of mathematics. Here are some links about all this, along with a few things I found especially interesting. In addition, in May the “unit distance conjecture,” one of Erdős’s problems, was solved by AI.

Navier-Stokes Millennium problem

• On the Navier–Stokes Millennium Prize Problem - The official OpenAI announcement, with a description of the problem and their results.
• PDF of the original paper
• How Terry Tao Became an Evangelist for AI in Math - An article in Quanta Magazine about computer-assisted proofs. “With automated proof-checkers, a problem can be broken up into small chunks, solved bit-by-bit, then reassembled with confidence that every piece is correct. For some, this heralds a new area in mathematical research.”
• Terry Tao’s blog - “Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao.” A great source of information related to computer-assisted mathematics.

Erdős problems

• Erdös problems - Lately, there have been several AI-assisted proofs of some of Erdős’s conjectures. This site has a lot of information on all of the propositions, including what they say, their current status, etc. This page lists all propositions and their current status.
• Erdős problems in the OpenAI proofs - This post discusses the problems that appear in this week’s OpenAI publication. From the post: “On Tuesday 6th October, OpenAI released a GitHub repository containing 372 significant proof claims in mathematics; most of them (claiming to) solve or make significant progress for important problems from across pure mathematics. This includes many Erdős problems. In this blog post I will, for the convenience of others, list the claims relevant to this site, and give some very brief remarks. Please use the comments to this blog post for a general discussion on this release.”
• The unit distance conjecture solved by OpenAI - One of Erdős’s problems was solved by AI in May 2026: “The unit distance problem asks for the maximum number of pairs of points at unit distance among $n$ points in the plane. The best known upper bound is $O(n^{4/3}),$ and the best known lower bound is $n^{1+C/\log \log n}$ for some constant $C>0$. The problem was posed by Paul Erdős in 1946, and has been a central problem in combinatorial geometry ever since. In May 2026, OpenAI announced that they had solved the problem using a combination of machine learning and traditional mathematical techniques.”

The statement of the problem is straightforward:

Let $u(n)$ be the largest possible number of unit-distance pairs among $n$ points in the plane. Examples attaining linear growth rate are easy to construct: placing $n$ points in a line gives $n - 1$ pairs, while a square grid gives about $2n$ pairs. The previously best known construction, coming from a rescaled square grid, turns out to give even more: $n^{1 + C / \log \log n}$ for a constant $C$. Since $\log \log n$ tends to infinity with $n$, the additional term in the exponent tends to $0$, meaning these constructions achieve growth only slightly faster than linear. For decades, it was widely believed that this rate was essentially the best possible, and no construction could improve significantly over the square grid. In technical terms, Erdős conjectured an upper bound of $n^{1+o(1)}$ in which the additional $o(1)$ indicates a term tending to $0$ with $n$. Our new result disproves this conjecture. More precisely, for infinitely many values of $n$, the proof constructs configurations of $n$ points with at least $n^{1+\delta}$ unit-distance pairs, for some fixed exponent $\delta > 0$.

+370 math articles

• GitHub repo with +370 mathematics papers - “This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.”
• Mathematics manuscript collection - Manuscript map: each result description is followed by its constituent manuscripts and their abstracts. Paper titles link directly to PDFs.
• Regular trajectories, pruning and quantum parity - There are a couple of quantum-circuit-related propositions in the list. This is one that might be interesting to revisit. Abstract: “We prove that constant-depth quantum circuits with arbitrary one-qubit gates and unbounded-arity Toffoli gates cannot compute parity with any fixed positive worst-case advantage using polynomially many total qubits. Ancillary qubits are initialized to $|0⟩$, one output qubit is measured, and all other final registers may be discarded without restriction. This resolves Moore’s parity conjecture in the measured-output model.”
• Exact quantum factoring over a fixed finite gate set - This is the most interesting one to me because it’s a problem I’ve worked on. It claims: “We give a polynomial-time uniform quantum circuit family that outputs the complete prime factorization of every integer N ≥ 2 with probability one. A fixed finite set of bounded-arity gates suffices, and both the gate count and the number of qubits have polynomial worst-case bounds in the input length.”

Other related proofs

• Astra and Claude Credited on Lean Proof of 11-Square Packing - “A GitHub repository called 11SquaresFormalized went up on October 6, with all 7,920 of its local Lean modules verifying and zero admissions in the final audit. The claim: that the arrangement of eleven unit squares inside a larger square that Walter Trump found in 1979, side length roughly 3.87708359002281, really is the smallest one possible.”
• The problem: pack 11 unit-length squares inside a larger square in the tightest possible way. The solution was found in 1979 by Walter Trump, but it took until 2026 to formally verify the proof using Lean.
• The arrangement found by Walter Trump in 1979 and the key points:
  • The Side Length ($s$): The enclosing square has a minimum side length of $\approx 3.877084$. This exact boundary is defined by a root of a degree-8 polynomial ($s \approx 3.87708359...$).
  • The Arrangement: The solution is highly non-intuitive. Instead of aligning all pieces straight, it contains six axis-aligned squares and a rigid block of five tilted squares.
  • The Tilt Angle: The five tilted squares are not turned at an obvious $45^{\circ }$ angle; they are strictly rotated at approximately $40.181937^{\circ }$ relative to the outer borders.
  • Rigidity: The layout is completely rigid, meaning there is zero room to slide or shift the individual unit squares to shrink the outer border any further. Even in this perfect configuration, only about 73% of the large square’s area is filled, leaving the rest as unavoidable empty space.
• The Fibonacci geometry of eleven squares - This paper seems to present a transformation that turns the convoluted solution into a more harmonious one. The paper is very hard to follow, though, so I’m not entirely sure that’s what it does. I want to revisit it.
• A Chiral aperiodic polygon with Fibonacci monodromy - This paper describes a chiral aperiodic 27-gon monotile. It differs from the now-famous “Hat” monotile in that it does not require both left and right versions of the tile. There is already a chiral aperiodic monotile called “Spectre,” so I’m not sure what the advantage of this one is. See here for more information about the “Spectre.”

Related links

• TactileJS - A JavaScript library for representing, manipulating, and drawing periodic tilings of the plane.
• Frag - A simple 2D fragment shader viewer, inspired by Shadertoy
• Personal page of Craig S. Kaplan - One of the creators of the ‘hat’ monotile.
• The blog of Dave Smith - The blog of Dave Smith, one of the creators of the ‘hat’ monotile.
• Cool apps for tiling - This directory has a lot of JavaScript apps to test tilings. It was created by Arnaud Chéritat

---

Build a $40 WiFi e-reader

An ESP32-S3, an e-paper panel, five buttons, and a scheduled agent that writes the morning brief. Roughly $40 in parts and a weekend.

• GitHub repo - An open-source ESP32-S3 e-reader with a 5.76-inch e-paper panel, a Game Boy and NES game server for your phone, and a live Pokémon companion dashboard on the e-ink.

---

More DIY audio projects

Here are a few more beautiful DIY audio projects I found.

• CD Transport - Here’s a CD transport project inspired by the Shigaraki player. An in-depth discussion can be found here: https://www.diyaudio.com/forums/audio-sector/160373-cd-transport.html

• SPDIF and USB DAC - The SPDIF DAC has been around since 2005, and there are a few reviews on 6moons; the most recent one is here: http://www.6moons.com/audioreviews/a…e5/system.html

• DIY community forum - A forum for DIY audio projects and DIY audio gear.

• Minimal modular amplifiers - This guy builds minimal amplifiers without a PCB. In this project, the amp is based on the LM3886 chip, and he builds a separate power supply. The complete amp, without the power supply, uses only 4 resistors, two caps, and an LM3886 amplifier chip (per channel)!

---

Poster prompts

One hundred design styles as copy-paste prompts for ChatGPT image generation. Each page shows the prompt alongside an example of what it produces — for two events: a village fête and a music gig.

Some look great, in my opinion. Others still look like slop, but with some tweaking they could work for a specific event. Taken together, they demonstrate the breadth of styles available. I recognise that almost all of the styles are entirely inappropriate for a village fête. The point is to show what you can do for any event, and that you can ask for whatever style you want.

• Poster Prompts - It turns out ChatGPT can generate better art if you prompt it correctly. This site helps you write more accurate prompts to get different styles.

---

Watt: the lean desktop project

The premise is simple: idle should mean idle. Every wakeup, every poll, every fork on a timer is a watt the battery doesn’t give back. Two sister suites grew out of pulling on that thread — CHasm in pure x86_64 assembly that paints the pixels and reads the keys, and Fe2O3 in Rust on a shared TUI foundation that does mail, files, calendars, charts, and the rest. Together they form a complete Linux desktop that idles at under three watts with the screen on and lasts about a day on a single charge. Pick a door.

• Watt website - The main site
• Geir Isene GitHub page - The author of the two repos.
• Nomad - The Android companion - The mobile half of the Fe2O3 suite. One Rust core, seventeen Kotlin / Compose apps, synced over Syncthing, with no Google account and no cloud middleman.

---

Encyclopædia Britannica

This site hosts the eleventh edition of the Encyclopædia Britannica (1910-1911).

• Site with the Encyclopaedia - You can browse all the articles, with both the text and a photograph of each page.
• Download the content - You can download the .md content of all articles. You can also buy an ebook version.

---

Sega Genesis trackers & other links

Here are two cool-looking native trackers for the Sega Genesis.

• MD.Tracker - Native music tracker for SEGA MEGA DRIVE / GENESIS / NOMAD

• genmddj - An LSDJ-inspired music tracker for the Sega Mega Drive / Genesis, driving the YM2612 FM synthesiser (6 × 4-operator + an 8-bit PCM DAC) and the SN76489 PSG (3 squares + noise), written in 68000 + Z80 assembly. It’s a sibling project to SMSGGDJ, little-scale’s Sega Master System / Game Gear music tracker.

• Sega Genesis/Mega Drive VDP Graphics Guide v1.2a (03/14/17) - A nice write-up of the Sega Genesis VDP.
• Retro game dev blog - Some nice articles related to retro game development.

---