Post #530690

https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html what I keep thinking about Claude translating zlib to Lean and proving it correct is that the Lean translation was proved correct but the C library is in the one deployed. Subtle but important. System software sometimes has perf edges that are not captured by the proof model, or scientific software has convergence edges, so a rewrite is risky to deploy as it will break something even if it is mathematically more certainly correct. Still, great progress in formal methods. Good reasons for optimism.