dca2

The cheap ones definitely do! The flagship models tend to be pretty decent.

I've been doing almost exactly this with Mafia (aka werewolf): running games where LLMs play against each other, with humans able to share the lobby. It's been a hit on family game night so far, because it allows our group to "fill out the cast" with a lot more characters than just the human players and add a lot of variety without needing a huge group.

My experience is that text-first, turn-based games are a particularly natural interface for LLMs vs graphical games (though you can provide a harness of course). They read a transcript, maintain a theory about what the other players know, then speak or choose a structured action. The important architectural problem is to represent the game state and actions in a way they can do successfully, particularly for cheaper models. But with a few human players + a frontier model or two + a backfill of cheap extras to provide chaos, it is super fun.

My favorite failure so far was a Kimi player getting fact-checked by the group, switching into third person, and concluding that the case against itself was compelling. So it voted for itself to be eliminated.

I collected a few examples here: https://botmafia.games/#emergent. No public instance yet, as I'm having fun iterating ideas on game nights, but it provides some flavor of what kinds of fun I've been having.

As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.

Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.

The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.

At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.

https://sealedabstract.com

Location: Austin, TX

Remote: Yes

Willing to relocate: No

Technologies: Swift, iOS, Rust, Apple platforms

Résumé/CV: On request

GitHub: https://github.com/drewcrawford

Email: drew@drewcrawfordapps.com

I'm a senior iOS developer with 15+ years of experience, mostly contract/freelance. I've done everything from pixel-perfect GUI implementation to SDK design, reverse engineering, Metal/Vulkan, algorithm design, low-level systems programming, optimization, debugging GPU drivers, porting, leading technical teams, architecture, app review, server-side Swift/Rust, WASM, and pretty much anything that touches a mobile app or Apple technology.