Project idea: formalize error correcting codes in Mizar.

Error-correcting codes are a beautiful subject, mostly because they're linear algebra over finite fields (and linear algebra is beautiful).

But there are exceptional connections in the subject: the Golay code and the Leech lattice especially connect with disparate subjects.

To give one sense of connection, I gave Robert A Wilson's construction of the Leech lattice using the octonions as a "milestone".

#Mizar #ProofAssistant #ErrorCorrectingCodes #LeechLattice #LinearAlgebra #Octonions #GolayCode

https://thmprover.wordpress.com/2025/01/09/from-error-correcting-codes-to-the-leech-lattice/

Does anyone know of any analytic approximations for the relationship between the efficiency of either a) source/compression coding algorithms, b) channel/error-correction coding algos, or even c) rate-distortion curves *AND* their computational/Big-O complexity (time or space)?

#infoTheory #rateDistortion #computationalComplexity #bigO #compression #errorCorrectingCodes #tractability #Shannon