这几个开源模型里Gemma 4最会写Coq证明，但100道题也只过12道，别指望它们太靠谱。
一项初步研究让6个开源权重LLM各尝试证明CoqStoq基准中的100个定理，每个定理只有一次机会，温度设为0，并用Coq内核验证结果。Gemma 4成功验证12个定理，Llama 3.3验证8个，DeepSeek Coder V2 Lite验证1个，Qwen 3.5、Mistral Small 3.1和GPT-OSS均未通过验证。全部21个成功结果覆盖15个不同定理，其中11个是标准Coq策略未能解决的。所有被验证的定理都只有短或中等人写参考证明，长证明定理无一成功。600次尝试中共产生21个内核验证证明，总体成功率3.5%。
Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study
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 proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.