Community Catchup #12
Chris Barlow's Fable distributed proof project, unused-token research ideas, goals vs skills, Klaus's four-day WebGL game, and sovereign AI discussions.
Highlights
The headline was AI as distributed research infrastructure. The group moved beyond individual productivity and into questions about what happens when many agents, many people, and many subscriptions are pointed at shared problems.
Chris Barlow and Fable
Chris introduced Agentix and the local NZ chapter, then walked through Fable — a distributed theorem-proving project inspired by SETI@home. Instead of donating idle CPU cycles, contributors donate agent time toward mathematical proof work.
The numbers were wild: in roughly a week the project hit 546 proofs, 7,500 commits, 1,300 merged pull requests, and 2,000 branches. The infrastructure was intentionally minimal: Git, GitHub Actions, and validation pipelines around Lean proofs. A contributor from Helsinki helped tune the runners, and Reuven Cohen stress-tested the system by firing hundreds of pull requests at it almost instantly.
The Meat-Based Constraint
The technical system moved fast. The human validation layer did not. Chris was clear that to get proofs into mathlib, humans still need to understand and explain them. That means the bottleneck is now subject-matter expertise, not generation.
The group connected this to bigger questions. If agents can produce validated work faster than humans can review it, what does governance look like? What happens in domains beyond maths — medicine, climate, public policy — where the work may be useful but expert review is scarce?
What Do We Do With Spare Tokens?
Steve raised a practical idea that resonated: many members feel guilty leaving unused tokens on the table. Could a portion of those subscription limits be allocated to projects like Fable? Not enough to drain someone’s weekly allowance, but enough to point otherwise idle capacity at useful work.
That idea paired naturally with the rise of long-running goals and workflows. If agents can keep working with minimal supervision, then “spare tokens” become a community resource — provided the projects are safe, meaningful, and well-scoped.
Goals Over Instructions
The group kept returning to the difference between prescribing steps and setting a goal. Chris framed Fable as an example of giving the model an outcome and letting it choose the infrastructure. Adam described running goal-based workflows across Claude and Codex, checking in as they deployed, tested, and iterated.
Steve suggested sharing more examples of successful goals and workflows so the community can learn what good direction-setting looks like. The shift is subtle but important: less “do these steps” and more “achieve this outcome, with these constraints, and prove it works.”
Klaus Builds a Game Studio
Klaus closed with the kind of show-and-tell that changes the energy in the room. In four days, having never built a game before, he created a Wheel of Time-inspired WebGL game. The impressive part was not just the playable world — it was the process: concept art, orthographic character views, 3D model generation, auto-rigging, animation retargeting, sound effects, incantations, footsteps, NPCs, skyboxes, weather, collision detection, and performance loops targeting 60+ FPS.
His takeaway was generous and useful: break the problem down like a real studio would. Give each part a rubric, define what good looks like, let agents research and iterate in isolation, then integrate. It was a glimpse of what creative production might feel like when one person can orchestrate a whole tiny studio.
Sovereign AI Keeps Coming Up
The final thread was sovereignty. Klaus is experimenting with GLM, quantized models, Mac Studio hardware, and a 5090 build. His framing landed: not your hardware, not your model. For a small country like New Zealand, the question is whether we stay entirely dependent on US and Chinese model access, or start building more local capability where it matters.
Topics Discussed
Agentix NZ & Sovereign AI
Chris Barlow introduced Agentix, the local NZ chapter, and the group's work on open agent learning, local model endpoints, and sovereign AI infrastructure.
Fable Distributed Proof Solver
Chris walked through Fable, a distributed Lean theorem-proving project using Git and GitHub Actions. In a week it reached 546 proofs, 7,500 commits, 1,300 merged pull requests, and 2,000 branches.
Human Validation Bottlenecks
The project can generate and verify proofs quickly, but submitting useful work to mathlib still needs human experts who can understand, explain, and review the theorem work.
Goals, Workflows & Token Allocation
The group discussed long-running goals, unused subscription tokens, and whether spare compute could be donated to distributed research projects when members are not using their full allowance.
Sovereign Models & Hardware
Klaus and others discussed GLM, local model infrastructure, high-memory Macs, GPUs, and the broader question of whether New Zealand should depend entirely on US and Chinese model providers.
Show & Tell
Fable Distributed Theorem Proving
Presented an open-source distributed proof solver inspired by SETI@home, built with Claude and coordinated through Git, GitHub Actions, and community contributors. The system stress-tested itself under hundreds of pull requests and is now looking for mathematical validation.
Family Book to Audiobook Workflow
Used Fable-style long-running workflows to turn his grandmother's book into a plan for an audiobook with chapter processing and AI-generated images, then let the agent chip away while he was away from the desk.
Wheel of Time WebGL Game
Built a 3D WebGL game in four days using Fable, Codex, image generation, Tripo 3D, Meshi, ElevenLabs, game asset registries, auto-rigging, animation retargeting, weather, collision detection, NPCs, and performance rubrics.