Diffusion-Proof es el primer marco para entrenar y aplicar modelos de lenguaje de difusión para la demostración formal de teoremas. Introduce dLLM-Prover-7B para la escritura completa de pruebas con coherencia a largo plazo y dLLM-Corrector-7- para la corrección local de pruebas utilizando información bidireccional. El marco supera las líneas base de LLMs autoregresivos en un 1.61% en ProofNet-Test y un 6.14% en MiniF2F-Test, y resuelve un problema del IMO más allá de la capacidad de DeepSeek-Prover-V2-7B.