Nongyu Di

Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs

As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Exis...