iiinova — where your digital self keeps evolving

Reposted by rntz

Hillel @hillelwayne.com · 15/09/2026

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

1242

rntz @rntz.net · 15/09/2026

book haul book haul (moe's books, berkeley)

five books:
Osamu Dazai - No Longer Human
Iain M Banks - The Hydrogen Sonata
Jacqueline Harpman - I Who Have Never Known Men
Bejamín Labatut - When We Cease to Understand the World
Ursula K Le Guin - Changing Planes

170

Reposted by rntz

Roly Perera @dynamicaspects.org · 13/11/2025

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.org

Galois Slicing as Automatic Differentiation

Galois 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 ...

161

Reposted by rntz

Red Blob Games @redblobgames.com · 14/09/2026

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.

4284

rntz @rntz.net · 12/09/2026

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.

150

Reposted by rntz

Mark J. Nelson @mm-jj-nn.bsky.social · 12/09/2026

Recent mechanized-proof news makes it interesting imo to revisit this paper from just a few months ago: Martens et al. "Is truth futureproof? On the possible futures of mechanized proofs". PLATEAU '26.

khoury.northeastern.edu

042

rntz @rntz.net · 12/09/2026

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.

020

rntz @rntz.net · 11/09/2026

I worry about incentives. How do we reward people, career-wise, for doing that work of explanation and socialization, if it becomes decoupled from novel results/proofs? At least in my academic field, papers with novel results are a primary currency for getting jobs, tenure etc.

100

rntz @rntz.net · 11/09/2026

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.

240

rntz @rntz.net · 11/09/2026

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!)

120

rntz @rntz.net · 11/09/2026

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.

120

rntz @rntz.net · 11/09/2026

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.

110

rntz @rntz.net · 11/09/2026

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?

110

rntz @rntz.net · 11/09/2026

Terence Tao & co have a statement on math & AI: mathandai.org. To me it suggests an emendation of Goodhart: aligned goals diverge under optimization pressure. Once, solving open problems required communal understanding; now, LLMs solve them without contributing back to the mathematical community.

mathandai.org

Declaration — Math and AI

Read the declaration and add your name.

150

Reposted by rntz

Nathan Lambert @natolambert.bsky.social · 11/09/2026

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.com

A Severe Misalignment of AI in Mathematics

I 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…

44515

rntz @rntz.net · 11/09/2026

chatgpt alone has looked on beauty bare

011

Reposted by rntz

BeijingPalmer @beijingpalmer.bsky.social · 17/08/2026

the entire Chinese internet has embraced what's basically a work of outsider art; a terribly animated film about a cow's dream made by a mother-son team and distributed by a former interior decoration company. It's now made millions at the box office.

131987589

rntz @rntz.net · 13/08/2026

would you accept 10 more years of your life if 9 of them were torture? I'm not convinced by this particular point. it seems to me suffering is unconditionally bad, regardless of mortality.

100

rntz @rntz.net · 13/08/2026

I was listening to the local classical music radio station and I was like "wait a minute... is that SANDSTORM by DARUDE?!" and it's pretty close! compare: 0:00-0:05 American Symphony III "Rondo", Adam Schoenberg www.youtube.com/watch?v=ShVo... 0:09-0:14 Sandstorm www.youtube.com/watch?v=y612...

youtube.com

American Symphony: III. Rondo

YouTube video by North Texas Wind Symphony - Topic

010

rntz @rntz.net · 11/08/2026

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.

000

rntz @rntz.net · 11/08/2026

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.

140

Reposted by rntz

Ray Vallese @rayvallese.bsky.social · 23/07/2026

There are ways to trim your videogame development budget, and then there are *ways* to trim your videogame development budget.

Screenshot from the videogame Grey Skies. A female character stands in front of an indoor swimming pool. A sign by the pool says PLEASE DO NOT SWIM, and, in smaller letters, "There isn't an animation for it."

5071331681

rntz @rntz.net · 23/07/2026

aaahhh, much better

the same diagram, arranged differently, looking much more visually symmetric

020

Reposted by rntz

Audrey @parickards.bsky.social · 16/07/2026

Yesterday...Northwestern Ontario looked like a scene straight out of Dante’s Peak.

26040971231

rntz @rntz.net · 15/07/2026

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

010

Reposted by rntz

Kiran @kirancodes.me · 06/04/2026

never writing latex by hand ever again. You are not ready.

914718

rntz @rntz.net · 01/07/2026

"fully propositional query language"? what does this mean?

100

rntz @rntz.net · 30/06/2026

my younger self is horrified rn

screenshot of a code editor showing six closing braces/dedents in a row each on separate lines

120

rntz @rntz.net · 29/06/2026

back to my favorite medium for thought

290

Reposted by rntz

Ann Leckie @annleckie.com · 29/06/2026

Out on the morning's Walk Fitness with Fitness Coach Vanburen, I was thinking of this, as I sometimes do: news.lettersofnote.com/p/she-was-th...

news.lettersofnote.com

She was the music heard faintly at the edge of sound

The Letters of Raymond Chandler

45911

rntz @rntz.net · 26/06/2026

zen and the department of cryptid zoology

000

Reposted by rntz

Ethan Mollick @emollick.bsky.social · 19/06/2026

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.

17411127

rntz @rntz.net · 19/06/2026

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.

000

rntz @rntz.net · 19/06/2026

the flipside: you can match the perceptual brightness or vividness (chroma) of two colors just by matching their L/C values. want a palette with uniform perceived brightness? with uniform vividness? easy! oklch.com and bottosson.github.io/misc/colorpi... are good for seeing the shape of colorspace

oklch.com

OKLCH Color Picker & Converter

OKLCH is a new way to encode colors (like hex, RGBA, or HSL)

110

rntz @rntz.net · 19/06/2026

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.

120

rntz @rntz.net · 17/06/2026

oklch is too good

150

rntz @rntz.net · 16/06/2026

Has anyone done domain theory for query languages? I have a new blog post about nontermination in query languages, why it poses a problem for query optimization, and three possible ways forward: www.rntz.net/post/2026-06...

rntz.net

Evaluation order and nontermination in query languages

050

rntz @rntz.net · 08/06/2026

tough audience here. do y'all not like puns or something?

010

rntz @rntz.net · 07/06/2026

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

131

rntz @rntz.net · 29/05/2026

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?

000

rntz @rntz.net · 27/05/2026

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?

040

rntz @rntz.net · 22/05/2026

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.org

miniKanren 2026 - ICFP 2026

The 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...

042