TY  - RPRT
TI  - Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
AU  - Ning Zhang
AU  - Nongyu Di
AU  - Zenan Li
AU  - Yuan Yao
AU  - Xiaoxing Ma
PY  - 2026
UR  - https://arxiv.org/abs/2606.17981
ID  - 2606.17981
ER  -