infotheo

Math foundations library

A Coq formalization of mathematical foundations for information theory and error-correcting codes

A Coq formalization of information theory and linear error-correcting codes

64 stars

6 watching

15 forks

Language: Coq

last commit: 6 days ago

convexityerror-correcting-codesinformation-theorymath-compmathcompprobabilityssreflect

Backlinks from these awesome lists:

Repository	Description	Stars
affeldt-aist/monae	A Coq library for formalizing and reasoning about monads with equational logic	68
affeldt-aist/coq-robot	A Coq-based library for formal foundations of 3D geometry and robot manipulators	26
math-comp/abel	Formalization of mathematical theorems about solvability and Galois theory for polynomials	28
unimath/foundations	A proof assistant library implementing univalent foundations of mathematics	240
vafeiadis/hahn	A collection of lemmas and tactics about lists and binary relations for a proof assistant	30
unimath/unimath	Formalizes mathematics using the univalent point of view	961
coq-community/fav-ssr	A comprehensive library of verified data structures and algorithms in Coq	45
stepchowfun/proofs	A personal repository of formally verified mathematics using the Coq proof assistant	291
choukh/baby-set-theory	A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs	43
coq-community/dedekind-reals	A formalization of Dedekind reals numbers in the Coq programming language	43
coq-community/gaia	A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics	28
math-comp/odd-order	Verifies a mathematical theorem in finite group theory	25
geohot/coq-hardy	Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory	53
math-comp/math-comp	A comprehensive repository of formalized mathematical theories based on Coq and SSReflect.	587