Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study

Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman +1

Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each pro…