rntz

rntz

@rntz.net

Michael Arntzenius irl. Postdoc at UC Berkeley doing PL + DB + incremental computation. PL design, math, calligraphy, idle musings, &c. rntz.net 🐘 @rntz@recurse.social 🐦 @arntzenius Attempting to use bsky more now that people are showing up.

403 followers176 following386 posts

rntz reposted

Hillel
@hillelwayne.com

Right now the biggest barrier to AI-driven formal methods is that AIs are absolutely dogshit at coming up with good properties. I thought that was just a March 2026 thing but it seems to be a September 2026 thing too

rntz reposted

Roly Perera
@dynamicaspects.org

New preprint with Robert Atkey. This paper recasts Galois slicing (a program slicing technique) as a kind of automatic differentiation, with lattices of slices corresponding to tangent spaces, and forward and backward slicing corresponding to forward- and reverse-mode AD. arxiv.org/abs/2511.09203

arxiv.orgGalois Slicing as Automatic DifferentiationGalois slicing is a technique for program slicing for provenance, developed by Perera and collaborators. Galois slicing aims to explain program executions by demonstrating how to track approximations ...

rntz reposted

Red Blob Games
@redblobgames.com

I am *loving* this use of LLMs. For my current project I'm writing all the code myself, but I have llm-buddy reading my code as I type, giving me feedback. And … it's caught a lot of bugs and style issues. It's telling me things I would've never thought of asking an LLM about.

Andrew Hyatt@andrewhyatt.bsky.social

I just posted a video introducing llm-buddy, with a demo showing how it detects issues in whatever you are writing in #emacs and how it can (optionally) just fix the issues that are too insignificant to mention.

rntz
@rntz.net

Do any proof assistants have a tool to get the "trust base" of a theorem, ie: 1. All defns transitively used by the thm statement; wrong definition -> wrong theorem! 2. Any postulates/axioms; anything proved by "sorry" &c. If not, why not? Seems essential for proof review.

View full thread
rntz
@rntz.net

This also shows AI alignment isn't just about aligning LLMs to their users or to "humanity", but about distinct groups' differing interests. I'm not sure what general conclusions to draw, but it makes me sympathetic to efforts to slow down or pause capabilities research.

rntz
@rntz.net

Daniel Lemire has a negative response to this statement, also worth reading: x.com/lemire/statu... I am sympathetic to his POV that LLMs will not destroy but only change mathematical inquiry. I think he focuses overmuch on credit; I worry more about culture and getting LLMs to aid understanding.

View full thread
rntz
@rntz.net

I think (a) is why Goodhart's law was observed and named in economic policy - capitalism provides a context of ruthless competition. I'm not sure how to generalize (b) to other domains, however.

rntz
@rntz.net

Separately, I hold out hope this is less a fundamental characteristic of LLMs than of AI arms-race/benchmark culture, and that used or trained differently, LLMs could be used to advance human understanding. (No doubt people are already mining the claimed Navier-Stokes proof for insights!)

rntz
@rntz.net

Taken literally, Goodhart's law suggests the Millennium Prize would make solving open problems useless as a measure of mathematical progress even pre-LLM; but this doesn't seem to have happened until now. Why?

rntz
@rntz.net

I think because it requires (a) ruthlessness: lack of backpressure against "gaming the system" (AI benchmark culture vs mathematical culture), and (b) raw ability - if it takes a long time to make progress, there's plenty of time for understanding to catch up.

rntz reposted

Nathan Lambert
@natolambert.bsky.social

A great read. I have similar feelings about how AI labs approach progress directly and without nurturing of scientific communities & intuition. The math research community went through the transition the fastest, so it was felt most. Other fields next. terrytao.wordpress.com/2026/09/11/a...

terrytao.wordpress.comA Severe Misalignment of AI in MathematicsI am proud to be among the list of 25 initial signatories — all Fields Medallists — to the declaration below, which grew out of discussions between ourselves over the last week. We have…
rntz
@rntz.net

I wish Rust had OCaml-style modules. Traits/typeclasses are great for structures over one main type. But ML modules don't make you feel like you're holding it wrong if you need to parameterize over lots of types none of which is the one main type. You just do it and move on.

rntz
@rntz.net

Instead I picked a convenient concrete type early on and now I want to change or parameterize over it, and I am in design hell ("is there a main type? should it be an associated type? which things need to be parameterized over this? what order?") and compiler error hell simultaneously.

rntz
@rntz.net

warm warm cat warm sunny cat happy warm sunny cat happy sunny cat happy sunny happy

rntz reposted

Ethan Mollick
@emollick.bsky.social

More evidence, from a large-scale study in China, that using AI hurts learning if it undermines mental effort. When homework time drops due to AI use, so do test scores. Across studies, there is a clear theme: AI tutoring in support of classes is good, using AI to "help" with homework is bad.

rntz
@rntz.net

this is not entirely ok-color-space specific; it's partly about irregular LCH-shaped color spaces vs cylinder-shaped HSL/HSV ones, and partly about prioritizing perceptual uniformity. eg. okhsl is cylindrical, and same saturation != same chroma, but you do get ~uniform lightness for fixed L value.

rntz
@rntz.net

the reason oklch is so good is also why it is inconvenient: it forces you to confront the fact that color space is weirdly shaped. want a bright, vividly saturated green? sure thing! want a blue or orange with the same brightness & vividness? TOO BAD.

rntz
@rntz.net

S tears of joy A tears of relief B tears of laughter C tears because of bright light D tears of pain F tears of grief

rntz
@rntz.net

So-called "parallel or", (x por y), terminates with true iff either x or y does, unlike "x or y" which diverges if x does. What about "parallel and": false and x = false x and false = false true and x = x x and true = x Is there a canonical or useful reference for either of these?

rntz
@rntz.net

I followed the instructions from https:// lean-lang.org/install/ to install lean via VSCode and create a first project with mathlib, and then I ran $ du -hs first-project/ 7.0G first-project SEVEN GIGABYTES what the fuck is going on here? who the fuck thought this was ok?

rntz
@rntz.net

The miniKanren and Relational Programming workshop is accepting submissions until June 5th! You (yes you!) should submit! We accept short or long papers, about miniKanren or relational programming more widely - and, this year especially, about relating the two! :) icfp26.sigplan.org/home/minikan...

icfp26.sigplan.orgminiKanren 2026 - ICFP 2026The miniKanren and Relational Programming Workshop is a workshop about relational programming with an emphasis on the miniKanren family of languages: miniKanren, microKanren, core.logic, OCanren, Guan...