AI-Powered Translation of Logical Foundations Textbook Achieves 350x Speed-Up in Verified Software Engineering

We present lf-lean, a verified translation of all 1,276 statements of the Logical Foundations textbook from Rocq to Lean, produced by frontier AI with ~2 person-days of human effort versus an…