Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

Vasily Ilin, Brian Nugent

Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this dist…