Gwern argues Lean-trained LLMs will have superior scaling exponents, eventually justifying large-scale software rewrites

Newest from @gwern who also called the importance of the scaling paradigm right after GPT-3:

"In particular, the Lean programming language likely has, with 2026-era LLMs, a worse baseline constant and total loss on existing codebases, but better scaling exponents. This would imply that implementations in Lean can eventually win and deliver large benefits in program correctness at global scale—and thus could help justify large-scale investments in rewriting existing codebases in Lean or paying for new Lean code, thereby improving global cybersecurity."