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

131990589

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

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

5071351681

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 · 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 · 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 · 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

Reposted by rntz

Zach Weinersmith @zachweinersmith.bsky.social · 12/05/2026

Interesting data from Pew on use of Ai by race/ethnic categories and by wealth. www.pewresearch.org/internet/202... Broadly speaking the more social privilege you have the less likely you are to use Ai for help.

915935

rntz @rntz.net · 09/05/2026

a Python gist explaining why this closed form formula for the nth prime works and also why it's inefficient and not very useful (90 lines with comments): gist.github.com/rntz/216cef1...

gist.github.com

An explanation of a closed formula for the nth prime number and why it's not very interesting

An explanation of a closed formula for the nth prime number and why it's not very interesting - closed_form_for_primes.py

240

Reposted by rntz

pete rodrigue @peterodrigue.bsky.social · 07/05/2026

If you take all the parking spaces in DC and add up their area, they would cover over 8 square miles, or the equivalent of 3 Rock Creek Parks.

A map showing an ~8 square mile box overlaid on DC, representing (most of) DC's many parking spaces.

163

rntz @rntz.net · 06/05/2026

I have a new paper! "Finite Functional Programming" combines functional programming with relational/tensor algebra using functions of finite support: Datalog relations are finite boolean functions; tensors are finite real-valued funs. arxiv.org/abs/2604.26161

arxiv.org

Finite Functional Programming

We unify functional and logic programming by treating predicatesas functions equipped with their support: the set of inputs whose output is nonzero. Datalog, for instance, is a language of finitely su...

1162

rntz @rntz.net · 06/05/2026

conjecture: well-moded bottom-up logic programming is about degree constraints in the sense of arxiv.org/pdf/2504.02770. R(x,y) has deg(y|x) < n iff ∀x. |{y:R(x,y)}| < n. If we relax this to ∀x.{y:R(x,y)} is finite, we're giving it mode R(x-, y+): if x is input, y is output.

arxiv.org

120

rntz @rntz.net · 29/04/2026

does the powerset monad distribute over the stream/possibly-infinite-list monad? (in the category theoretic sense of a distributive law of monads)

100

rntz @rntz.net · 17/03/2026

I have muted the thread that was in the TYPES list on which you were probably expecting a subskeet Forgive me it was predictable so long and so dull

030

rntz @rntz.net · 17/03/2026

> ghc foo.hs -outputdir ~/.Trash highly sus... yet oddly useful

010

rntz @rntz.net · 16/03/2026

A little haskell command-line script to calculate good, small rational approximations of real numbers. Eg: approximating 0.13 yields 1/7 ≈ 0.1429, 1/8 = .125, 3/23 ≈ 0.1304, 13/100 = 0.13 in that order. Useful more often than I expected. gist.github.com/rntz/6713db2...

171

rntz @rntz.net · 09/03/2026

for a while there I thought silksong had integrity and then I found the goddamn double jump

020

rntz @rntz.net · 02/03/2026

behold the quality of my commit messages

* 1e3b8d6 work
* be68869 work
* f78da1b work
* 7f85b0b work
* f145b04 Update on Overleaf.
* 751966e work
* 7e34a6c work
* 9cbac47 work
* a037082 work
* ec99d61 work
* b292429 work
* 908f2fe work
* f02ff83 work
* 2b7dd67 work
* e6d36af work
* 570e91a work
* c458a82 work
* 78966a5 work
* dbc0cd6 work
* 09f6b18 work
* 43e4d6c work
* 0ec0ce8 work
* bdcdadb rm sections.tex
* 9f9e18e add sections.tex
* 47f8674 work
* aa3b55e work
* 7ec0caf work

4100

rntz @rntz.net · 28/02/2026

Functional programming couples functional dependency (for fixed x, y there's at most one z = x + y) with input-output directionality (supply x,y to get z). Logic/constraint programming decouples them: what are the x, y such that x + y = 5?

140

rntz @rntz.net · 23/02/2026

1000xresist is a helluva game

020