Cover image

When Coders Prove Theorems: Agents, Lean, and the Quiet Death of the Specialist Prover

A coder does not trust a program because it sounds plausible. A coder runs it, reads the error message, changes the implementation, tests again, searches the library, asks a colleague, splits the problem, and keeps going until the machine stops complaining. That mundane loop is the interesting part of Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics.1 The headline result is easy to market: with Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all 12 Putnam 2025 problems in Lean, matching the reported perfect score of AxiomProver. Nice. The trophy cabinet sparkles. ...

January 21, 2026 · 20 min · Zelina
Cover image

Houston, We Have a Benchmark: When Agentic AI Meets Orbital Reality

Space is not impressed by fluent reasoning. A satellite does not care that an AI agent has produced a confident plan. A ground station cannot magically see through the Earth because the prompt says “ensure connectivity.” A sensor cannot keep collecting images after its onboard storage is full. Orbital mechanics, power budgets, slew angles, data buffers, and line-of-sight geometry are not stakeholder preferences. They are constraints. Reality, annoyingly, still has root access. ...

January 19, 2026 · 13 min · Zelina
Cover image

Seeing Is Not Thinking: Teaching Multimodal Models Where to Look

A model can see the image and still miss the point Inspection is a wonderfully cruel test for AI. Show a multimodal model a product photo, a medical scan, a factory defect, a form, or a dashboard screenshot, and the answer may sound calm, fluent, and technically plausible. The model may even imitate the reasoning style of a stronger teacher model. It may describe objects, infer relationships, and produce the correct-looking sentence. ...

January 18, 2026 · 17 min · Zelina
Cover image

When AI Stops Pretending: The Rise of Role-Playing Agents

A chatbot can act like a pirate for three turns. That is not the impressive part. A teenager with a Halloween hat can also do that. The harder problem begins when the agent has to remember what happened last week, preserve a recognizable personality across changing situations, make choices consistent with its motives, avoid borrowing another character’s copyrighted voice a little too enthusiastically, and still behave safely when the user pushes it outside the script. At that point, “pretend you are X” stops being a prompt trick and becomes a systems engineering problem. ...

January 18, 2026 · 16 min · Zelina
Cover image

MatchTIR: Stop Paying Every Token the Same Salary

Payroll is a useful metaphor for agent training because it makes the absurdity obvious. Imagine a project team where one employee finds the right database, another enters the correct query, a third repeatedly calls the wrong API, and a fourth finally writes the report. If the report is accepted, everyone receives the same bonus. If it fails, everyone receives the same blame. Very democratic. Also very stupid. ...

January 17, 2026 · 16 min · Zelina
Cover image

One Agent Is a Bottleneck: When Genomics QA Finally Went Multi-Agent

One Agent Is a Bottleneck: When Genomics QA Finally Went Multi-Agent Databases are where elegant AI demos go to develop a limp. A model can sound fluent about biology, medicine, finance, or law. Then someone asks a question that requires the latest record from a specialized database, a second lookup from another source, a formatted API call, a large HTML response, and a final answer that does not forget the original question halfway through. Suddenly the “AI assistant” becomes a very expensive intern copying URLs into the wrong field. ...

January 16, 2026 · 15 min · Zelina
Cover image

When Agents Talk Back: Why AI Collectives Need a Social Theory

Teams are easy to draw and hard to govern. Put five AI agents in a workflow diagram and everything looks reassuringly corporate: one planner, one researcher, one coder, one critic, one manager. Give them arrows. Add a dashboard. Call it orchestration. Investors relax. Engineers nod. Consultants quietly increase the font size on the word “autonomous.” ...

January 16, 2026 · 18 min · Zelina
Cover image

When Goals Collide: Synthesizing the Best Possible Outcome

A robot does not always get the luxury of a clean task list. Reach the loading bay. Avoid blocked corridors. Preserve battery. Pick up two packages. Respect a safety boundary. Finish before the door closes. Then the environment, as environments enjoy doing, changes the rules halfway through. A corridor shuts. A resource disappears. One goal now interferes with another. ...

January 16, 2026 · 16 min · Zelina
Cover image

EvoFSM: Teaching AI Agents to Evolve Without Losing Their Minds

Workflow is the unglamorous part of agentic AI. Which is precisely why it matters. A research agent can have a strong language model, a decent search tool, and an impressive ability to produce paragraphs that sound like a McKinsey intern who drank too much espresso. Yet when the task becomes long, ambiguous, and evidence-heavy, the same agent often fails for a boring reason: it does the right actions in the wrong order, repeats the same weak search, summarizes too early, forgets to verify a source, or changes its own instructions so enthusiastically that it becomes a different employee halfway through the job. ...

January 15, 2026 · 13 min · Zelina
Cover image

When Agents Learn Without Learning: Test-Time Reinforcement Comes of Age

A team meeting usually ends with someone saying, “Let’s remember this for next time.” Human teams sometimes do. Agent teams usually do not. A group of LLM agents can debate, critique, revise, and produce a final answer. Then the whole episode often disappears into the landfill of inference logs: useful comments, bad guesses, decisive objections, elegant checks, all flattened into “the model answered correctly” or “the model failed.” Very modern. Very wasteful. ...

January 15, 2026 · 17 min · Zelina