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/

Archiving Data On Paper Using 2D Images https://hackaday.com/2024/09/15/archiving-data-on-paper-using-2d-images/ #errorcorrection #hammingdistance #SoftwareHacks #laserprinter #datacoding #archiving #golaycode #scanner #qrcode #FEC