Skip to content
Sagan

Paper

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

Unreadunread

AI summary

arXiv:2606. 13925v1 Announce Type: new Abstract: 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.