A nice article on the arXiv: just because LLM-generated Lean proofs compile without "sorry" (essentially a gap that needs filling), it doesn't mean they're correct. It's too easy to get the definitions wrong. I think we all knew this, but it's great to see. #Lean #MathSky
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 distinction through a…
