Rocq Prover

Rocq Prover 是一种值得信赖的、工业强度的交互式定理证明器和依赖类型编程语言，用于数学、计算机科学等领域的机械化推理。