sigil

Great essay, thanks for sharing.

When I was a software library developer, I came to resent application developers. I noticed a pattern. Libraries solved hard problems and did so carefully, thoughtfully, in a way that others could reuse. Apps would come along and carelessly, recklessly glue together several high quality libraries into a piece of software targeting a general audience. The apps would then harvest all the credit.

What's happening in mathematics right now feels similar. Applications (theorems) were always how one built objective reputation, but libraries (concepts, definitions, boring lemmas) were also rewarded socially within the mathematics community. And individual mathematicians often managed to both build their own libraries, and use them to prove an important result. And then those libraries were sometimes of use in other results.

Bessis asks whether AI Lean proofs will land in Mathlib or Mathslop. Or in my framing: will they be libraries, or applications?

At present they're mostly Mathslop. The proven result is perhaps useful, but the methods employed aren't novel or reusable. I worry that this trend will only worsen, because applications make headlines, and the libraries they used do not. We are not properly incentivizing library development in OSS, or in math, or in infrastructure writ large. There's a serious credit assignment problem here.

What might change this? Once the low hanging fruit is picked, will citation count rise in relative status again? Will we get result fatigue and start to reward legibility — no one cares unless the paper has an accompanying ELI5 tiktok video? A labeling regime that certifies the proof was produced sustainably, organically, by local artisans with no AI additives?

There's a reason Spotify might force shuffle play on the free tier. It isn't solely to annoy you into upgrading. Royalties are 2x - 5x higher for interactive vs non-interactive streaming plays.

Are human rights concerns running cover for more straightforward financial interests here? Norway and Saudi Arabia are both petrostates with large sovereign wealth funds.

This nginx local dev config snippet is one-and-done:

  # Proxy to a backend server based on the hostname.
  if (-d vhosts/$host) {
    proxy_pass http://unix:vhosts/$host/server.sock;
    break;
  }

Your local dev servers must listen on a unix domain socket, and you must drop a symlink to them at eg /var/lib/nginx/vhosts/inclouds.localhost/server.sock.

Not a single command, and you still have to add hostname resolution. But you don't have to programmatically edit config files or restart the proxy to stand up a new dev server!

Gleick's "Chaos" got me sent to the principal's office in high school. I went crazy for fractals. Unfortunately all I had at home was an IBM PC XT. Mandelbrot set renderings were agonizingly slow and the CGA palette was too limiting.

Around this time my co-conspirator and I realized the library had 386s that almost no one was using for catalog search. They became our fractal render farm. We'd exit the catalog program, insert a floppy with our latest renderer, kick off a deep zoom, and turn off the monitors to avoid suspicion until we could check back next period. The results were thrilling. What a difference the access to compute made.

You all know the story -- eventually the librarian found us out and reported us for "hacking."

Thank you!