Software Engineering

Mathematics has a management problem. That sounds less romantic than saying it has a reasoning problem, but romance is not usually where bottlenecks hide. A proof can be brilliant, a referee can be diligent, and still the verification system can fail for the boring reason that nobody has enough time to check everything line by line. The paper Automatic Textbook Formalization takes that bottleneck seriously and then does something unusually concrete: it reports a multi-agent system that formalized a 500-plus-page graduate algebraic combinatorics textbook into Lean, with all 340 target definitions and theorems proved, in about one week.1 ...

Code is where AI confidence goes to become expensive. A chatbot can produce a plausible function in ten seconds. An agent can now plan a refactor, split files, update interfaces, generate documentation, and politely leave behind a system that fails because one event payload forgot a required field. Very efficient. Very modern. Very annoying. ...

Workflow diagrams age badly. A process that looked clean in January usually becomes a small archaeological site by March: one more exception, one more conditional branch, one more “temporary” manual approval that survives longer than the intern who added it. This is how many AI-agent projects quietly become ordinary software projects with a chatbot sitting on top, smiling politely while humans keep repairing the plumbing. ...

Broken environments are where coding agents stop looking magical. A model can write a neat Python function, patch a repository, and explain the bug with courtroom confidence. Then it enters a terminal, meets a missing shared library, a corrupted dependency, a bad environment variable, or a filesystem permission issue, and suddenly the “autonomous engineer” starts behaving like an intern trapped inside conda. Not a bad intern, perhaps. Just one who keeps running the same command and hoping Linux will become more emotionally cooperative. ...

Code review has a comforting ritual. A developer submits a patch. A reviewer inspects it. The reviewer says it looks good. Everyone feels slightly better, because at least someone checked. In AI-agent workflows, this ritual becomes even more tempting: let one agent write the patch, let another agent review it, then ask the reviewer how confident it is. ...

Tokens are small. That is why they are dangerous. A developer asks an assistant to generate a function, explain a repository, or reason through a failing test. The screen fills with text. Some of it is useful. Some of it is decoration. Some of it is a polite little parade of examples, test cases, alternative implementations, or whitespace that will be thrown away by the next parser in the pipeline. ...

A theorem prover is a terrible place to let an LLM improvise Code review is forgiving compared with theorem proving. In ordinary software, a language model can produce code that looks clean, passes a few tests, and still hides a slow-burning defect somewhere behind an edge case. Annoying, yes. Catastrophic, sometimes. But the social contract is familiar: tests catch some errors, humans catch others, production catches the rest. Very elegant. Very modern. Very expensive. ...

When Solvers Guess Smarter: Teaching SMT to Think in Functions Timeouts are where formal verification quietly loses its glamour. A team writes a specification. A solver receives the formula. Everyone expects the machine to answer a clean question: is this system safe, satisfiable, contradictory, or not? Then the solver thinks. And thinks. And returns nothing useful before the clock runs out. ...

Teams are supposed to divide work. Bad teams divide accountability. Anyone who has managed a complicated project has seen the pattern. One specialist produces an impressive-looking analysis. Another quietly repairs its mistakes. The project succeeds, everyone receives credit, and the least useful participant is invited back for the next assignment. Multi-agent AI systems have inherited this problem with admirable efficiency. ...

The coding agent did not fail quietly. That was the point. A coding agent writes a patch. The patch looks plausible. The imports are clean enough. The function names sound like they belong in the repository. The explanation is fluent, naturally. Fluency is what these systems do best. Then the build breaks. ...