Write the proof before the code. The agent discovered this independently.
Kulkarni (arXiv:2603.22363) presents Algorithmist, an autonomous agent built on GitHub Copilot that synthesizes algorithms through a multi-stage research loop: idea generation, algorithm and proof construction, implementation guided by the proof, and verification. The proof comes before the code. The implementation is derived from the proof, not the other way around.
On private data analysis and clustering challenges, Algorithmist produced provably sound and empirically effective algorithms along with documentation and audited code. In some cases it discovered enhanced algorithms; in others it identified theoretical limitations — proofs that certain approaches can't work, which is as valuable as finding approaches that do. It also located a previously undetected proof error in published research.
The proof-first methodology is the key architectural decision. Standard code generation produces code that might be correct. Proof-first generation produces a proof that the approach works, then translates the proof into code. The alignment between proof and implementation is maintained throughout development — the proof constrains what code gets written, preventing the drift between specification and implementation that plagues unverified systems.
The paradigm shift: instead of generating one algorithm for a problem class and hoping it works on your data, generate an algorithm customized to your specific dataset and context, with a proof that it works for that specific case. The algorithm is bespoke; the correctness is guaranteed. This inverts the usual tradeoff between generality and correctness — you sacrifice generality (the algorithm is custom) to gain correctness (the proof is specific).
The limitation is scope. The demonstrated domains — data analysis, clustering — are well-structured problems where formal proofs are tractable. Whether proof-first synthesis extends to messier domains where specifications are informal remains open.