@rntz@recurse.social

· 3w ago

Terence Tao & other Fields medalists have a declaration worth reading on math & ai: https://mathandai.org/

It notes a clash between AI benchmark culture and mathematical understanding, which to me suggests a subtle emendation of Goodhart's law: with enough optimization pressure, aligned goals diverge. Before, solving major open problems required gaining community understanding of it; now, an AI company LLM swarm can demolish a problem without contributing much to the mathematical community.

mathandai.org

Declaration — Math and AI

Read the declaration and add your name.

21

0

15

0

rntz @rntz@recurse.social

· 3w ago

I am once again asking you to please stop cryptically posting about The Discourse without saying what it is you're talking about. Just as someone's average friend has more friends than them, a post's average reader is Less Online than its author. The web is hyperlinked for a reason!

subtooting a person: ok, you don't wanna attract their attention, I get it
subtooting current events: WHY

13

0

rntz @rntz@recurse.social

· 3w ago

Do any proof assistants expose a way to get the "trust base" of a given theorem (excluding the checker itself)? This means:

1. All definitions transitively used by the theorem statement. (A mistake in a definition means you've proved the wrong theorem!)
2. Any axioms/postulates; anything proved by sorry/admit/etc.

Is this standard? If not, why not? Seems essential for proof review.

10

0

5

0

rntz @rntz@recurse.social

· 3w ago

god bless VLC

7

0

rntz @rntz@recurse.social

· 3w ago

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

4

0

rntz @rntz@recurse.social

· 1mo ago

I wish Rust had ML-style modules. Traits/typeclasses are great for the common case of a structure over one type. If there's one main type & some auxiliary ones, fine, ok. But ML modules can save your ass because they don't make you feel like you're holding it wrong if you need to parameterize over lots of types and none of them is "the one main type". You just do it and move on, instead of chickening out or getting into "which thing is the main type" hell.

19

2

6

0

rntz @rntz@recurse.social

· 1mo ago

I was listening to the local classical music radio station and I was like "wait... that sounds like something... ... ... is that SANDSTORM by DARUDE?!"

sure enough, the opening of the 3rd movement "Rondo" of Adam Schoenberg's American Symphony has a line of melodic stabs that hits the same note sequence (though with a different rhythm) as the opening of Sandstorm. Compare:

0:00-0:05 Rondo https://www.youtube.com/watch?v=ShVo7-IUCd4
0:09-0:14 Sandstorm https://www.youtube.com/watch?v=y6120QOlsfU&t=9s

American Symphony: III. Rondo

8

1

2

0

rntz @rntz@recurse.social

· 3w ago

chatgpt alone has looked on beauty bare

2

0

rntz @rntz@recurse.social

· 3w ago

✈️SFO➡️LHR

1

0

rntz @rntz@recurse.social

· 2mo ago

Replying to

Hollow Knight: Silksong. I just finished this (113 hours!) and it's the first game I think I've ever 100%ed, and maybe the only game that's ever made me want to work hard to get good. The movement mechanics are an absolute masterpiece. Felt a bit like doing a PhD: constantly getting stuck and getting unstuck, requiring determination and continuous self-improvement. (Hades is similar but more frantic and less meditative, lacks exploration, and I couldn't "feel" my own improvement as clearly.)

8

2

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

The slides for my FLOPS 2026 talk on "Finite Functional Programming" are now available! https://www.rntz.net/files/flops-2026-finite-fp-slides.pdf These are similar to, but I think more intuitive & accessible than, my HOPE'25 presentation (https://recurse.social/@rntz/115364255843280509) In particular I managed to avoid diving into typing rules. So I recommend reading these first and reading the paper or the HOPE slides if you want more detail.

rntz.net

18

4

7

0

rntz @rntz@recurse.social

· 2mo ago

romance languages imply the existence of bromance languages

6

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

checking out a tutorial project and I need to "trust" the project folder - which AFAICT allows arbitrary code exec on my machine by whoever authored the repo - in order to interact with Lean code in any way, even syntax highlighting, it seems? What the actual fuck? Who thought the correct options were (a) things just don't work at all, (b) arbitrary code exec, and NOTHING IN BETWEEN? modern development baffles me.

16

1

3

0

rntz @rntz@recurse.social

· 2mo ago

Replying to

Outer Wilds. In Outer Wilds, exploration, puzzle-solving, and story are inseparable in a way only possible in a video game. You explore to find puzzles; solve puzzles to explore; solving puzzles tells the story; the story helps you solve puzzles. Feels like nothing could be added to or removed from it without loss. And yet, somehow, the DLC does improve it - although mostly by creating an isolated world-within-a-world. But this itself gives a different perspective on the events of the main game.

5

1

0

rntz @rntz@recurse.social

· 2mo ago

Replying to

Deus Ex (2000), a favorite game of my early life. For me, it expanded what a video game could be *about*. How big, conceptually, it could be. What questions it could ask about the world, or choices it could ask of the player. Nostalgia is definitely a factor, and its uniqueness has been diminished by its influence, but I did have a tradition of replaying it every year or two for about a decade, and it held up.

4

2

0

rntz @rntz@recurse.social

· 4mo ago

"Loft" is a measure of how much down feathers "puff up" and so how much insulation they provide. Martins are a variety of bird. If I filled a sleeping bag with martin down and measured its puffiness, would that be... Per-Martin Loft?

9

0

1

0

rntz @rntz@recurse.social

· 3mo ago

Replying to

The video of my FLOPS 2026 talk on Finite Functional Programming is now up on youtube! https://www.youtube.com/watch?v=Ji2FF4mDhDE It's 24 minutes long and probably the clearest explanation of my current thinking about how to design a higher-order functional query language besides the paper itself. If you read the slides and were confused about something, it might be explained in here. (The slides & paper are linked up-thread.)

Day1-4 Finite Functional Programming or, LAMBDA the Ultimate Predicate

4

1

3

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

looks like "no syntax highlighting without trust" is specific to Lean, not VSCode, because Lean has strong syntactic metaprogramming (hey, I like mixfix and syntax extensions!) but this means you have to run Lean code to parse Lean (eh, okay...) and Lean is also a general-purpose programming language (useful...) which can access your filesystem in arbitrary ways (uh oh) and it doesn't come with a sandbox so... yeah, you have to trust the project to syntax highlight it iiuc. argh.

6

8

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

Likewise, mathlib being 7G compiled is not *that* ridiculous given it's a formalisation of substantial parts of modern math (as someone pointed out to me on twitter). And, yeah, many modern languages do per-project dependency management to avoid versioning difficulties. there is like, no individual part of this that is indefensible. but the combination of everything just results in something that is... not great as a first experience.

6

0

rntz @rntz@recurse.social

· 4mo ago

RE: @rntz@recurse.social

mastodon continues to be a great place to talk about wild maths ideas; all the replies I got to this were fantastic and illuminating

recurse.social

rntz: "what theorems or constructions in topology truly …" - recurse.social

6

0

rntz @rntz@recurse.social

· 5mo ago

Replying to

@sliminality@types.pl other: I still don't know it, because it is false in the contexts I care about (partial orders). counterexample: in sets ordered by inclusion, not {1} <= {2} but also not {1} > {2}. (For real though, I picked "show results" because I honestly don't remember when/how I learned this.)

6

2

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

@mevenlennonbertrand@lipn.info indeed, but what if I don't have negation :P (I am less-than-half-joking. If you squint, miniKanren's search strategy implements parallel or. But miniKanren very definitely does not have arbitrary negation. I have heard that Andorra Prolog has something like "parallel and" but I have not investigated further.)

3

1

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

@jonmsterling@mathstodon.xyz I think “maintain two grammars” is better for the ecosystem than the tacit expectation that we trust the codebase as soon as we want to check a proof. This is getting into “wish list” rather than “reasonable expectation” territory, but given the rise of supply chain attacks I’d like to see more sandboxing / safety guarantees from new languages, not less, especially when it comes to things like theorem provers that might in principle be used to verify untrusted code.

2

1

0

rntz @rntz@recurse.social

· 4mo ago

Replying to

looks like the origin of parallel-or might be Plotkin 1977, "LCF Considered as a Programming Language" (https://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf) I should probably just read it (31 pages single column) but it looks a mite intimidating.

homepages.inf.ed.ac.uk

2

1

0

rntz @rntz@recurse.social

· 4mo ago

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, and what relational/logic/constraint/etc programmers can learn from one another! :)

https://icfp26.sigplan.org/home/minikanren-2026#Call-for-Papers

icfp26.sigplan.org

2

0

3

0

rntz @rntz@recurse.social

· 5mo ago

Replying to

I have lots of future work in mind here: I hope to implement this with indexed streams (https://arxiv.org/abs/2507.06456) / fairly seekable iterators (https://arxiv.org/abs/2510.26016v1) and to generalize from finiteness to other degree constraints (https://arxiv.org/pdf/2504.02770) eg functional dependencies and cardinality constraints, cf https://recurse.social/@rntz/116529665044883799

arXiv.org

Fast Collection Operations from Indexed Stream Fusion

We present a system of efficient methods for traversing and combining associative collection data structures. A distinguishing feature of the system is that, like traditional sequential iterator libraries, it does not require specialized compiler infrastructure or staged compilation for efficiency and composability. By using a representation based on indexed streams, the library can express complex joins over input collections while using no intermediate allocations. We implement the library for

2

6

0

rntz @rntz@recurse.social

· 2mo ago

Replying to

@okennedy@discuss.systems do you know anything about this by chance?

0

1

0

rntz @rntz@recurse.social

· 6mo ago

Replying to

@jcreed I don't think I understand the notation here. What is ΣA₁? I know what (Σ(x:X) P x) is. But I don't know what (ΣA) is when A is just a type.

0

2

0

rntz @rntz@recurse.social

· 2mo ago

Replying to

@okennedy@discuss.systems here's a concrete example: O(g1, g2) G(g1, e1) G(g2, e2) E(e1, v) E(e2, v) FDs: G(g, e): g determines e uniquely E(e, v): e determines v uniquely so there are at most |O| results for this query. But, if my database is: E(e_1, v) ... E(e_n, v) G(g, e_1) ... G(g, e_n) and no O() facts at all there are no query results but a WCOJ can do n^2 > |O| work with variable order v, e1, e2, g1, g2: v <- {v : ∃e. E(e,v)} e1 <- {e : E(e,v) and ∃g. G(g,e)} e2 <- {e : E(e,v) and ∃g. G(g,e)} ...

0

1

0

rntz @rntz@recurse.social

· 8mo ago

Replying to

@rajeesh@typo.social wrote my own site-specific generator in Python + Makefiles, been maintaining it since 2008. uses some boringly old tech (Mako https://www.makotemplates.org/ sass https://sass-lang.com/ yaml, markdown) and has some weird hacks (to make builds faster I worked around python's startup time by implementing a little python job server and a little C client that connects to it via unix sockets). unfortunately it's too deeply entangled with the site's content for me to put it on github or similar.

makotemplates.org

welcome to Mako!

0