Coq

Coq 是一个正式的证明管理系统。 它提供了一种形式化的语言来编写数学定义、可执行算法和定理,以及用于机器检查证明的半交互式开发的环境。(Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.)

主要指標

概覽

名稱與所有者rocq-prover/rocq
主編程語言OCaml
編程語言Emacs Lisp (語言數: 17)
平台Mac, Windows
許可證GNU Lesser General Public License v2.1
發布數143
最新版本名稱V9.1+rc1 (發布於 2025-07-07 17:25:42)
第一版名稱V7-0beta (發布於 2013-11-18 18:55:31)
創建於2011-02-17 05:49:37
推送於2025-09-13 11:30:07
最后一次提交2025-09-12 15:10:28
星數5206
關注者數104
派生數691
提交數46595
已啟用問題?
問題數10348
打開的問題數2542
拉請求數8707
打開的拉請求數94
關閉的拉請求數1817
已啟用Wiki?
已存檔?
是復刻?
已鎖定?
是鏡像?
是私有?
去到頂部