欢迎使用 Coq 证明助手

Coq 是一款形式化证明管理系统，它提供了一种形式化语言来编写数学定义、可执行算法和定理，以及一个用于半交互式开发机器验证证明的环境。Coq 的典型应用包括编程语言属性认证、数学形式化和教学。Coq 拥有庞大而活跃的用户社区，为 Coq 的开发做出了贡献，包括正式开发、Coq 扩展和基于 Coq 的工具。Coq 是一个免费的开源软件，其开发主要由法国公共计算机科学机构 Inria 支持，任何人都可以在 GitHub 上关注和参与该过程。