proofs

Formal math proofs

A personal repository of formally verified mathematics using the Coq proof assistant

My personal repository of formally verified mathematics.

GitHub

292 stars
11 watching
12 forks
Language: Coq
last commit: almost 2 years ago
coqformal-verificationinteractive-theorem-provingproof-assistanttype-theory

Related projects:

RepositoryDescriptionStars
choukh/baby-set-theoryA Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs43
math-comp/coq-combiFormalizes algebraic combinatorics and symmetric functions in Coq.37
math-comp/odd-orderVerifies a mathematical theorem in finite group theory27
coq-community/coq-100-theoremsRepository tracking famous theorems proved using proof assistants.57
princetonuniversity/vstA collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant444
math-comp/abelFormalization of mathematical theorems about solvability and Galois theory for polynomials28
ejgallego/pycoqPython bindings for Coq's interactive proof assistant50
ilyasergey/pnpA tutorial project on using Coq to mechanize mathematics with dependent types160
choukh/set-theoryA formalization of set theory and its foundational axioms in the Coq proof assistant language59
discus-lang/ironFormalizations of functional languages with a focus on proof and verification142
huynhtrankhanh/coqcpVerifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof22
math-comp/math-compA comprehensive library of formalized mathematical theories593
coq/platformA multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching191
math-comp/analysisA Coq proof-assistant library for real analysis and mathematical structures210
yosuke-ito-345/actuaryFormalizes basic actuarial mathematics using Coq21