Capital de Tokens

Blog

Ideas, analysis, and independent articles from the channel and its episodes.

Blog RSS

What does it mean to formalize mathematics? Fermat, Lean, and the gap between human rigor and machine-checkable proof

Mathematics is already rigorous, but most proofs are not written with the level of explicit detail a computer needs. Anthropic's recent Lean formalization of Fermat's Last Theorem shows what changes when every definition, hypothesis, and logical step must be checkable by a proof kernel.

Your boss can already be an algorithm: what the gig economy reveals about the future of work with AI

Debates about autonomous agents usually look to the future, but Uber, DoorDash, and other platforms already show what happens when algorithms allocate work, set incentives, and can cut people off from their income. Princeton researcher Andrés Monroy-Hernández offers a more useful way to think about AI and work: not only as automation, but as a question of power, transparency, and platform design.

Codex Voice is becoming more than code dictation: a control plane for agents

The community is using Voice in Codex for something more interesting than talking to an editor: coordinating workers, checking progress, redirecting tasks, and working hands-free. We review real usage patterns, open problems, and the architecture this suggests for voice-driven development agents.