Alex Nelson<p>Project idea: formalize error correcting codes in Mizar.</p><p>Error-correcting codes are a beautiful subject, mostly because they're linear algebra over finite fields (and linear algebra is beautiful).</p><p>But there are exceptional connections in the subject: the Golay code and the Leech lattice especially connect with disparate subjects.</p><p>To give one sense of connection, I gave Robert A Wilson's construction of the Leech lattice using the octonions as a "milestone".</p><p><a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="tag">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="tag">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/ErrorCorrectingCodes" class="mention hashtag" rel="tag">#<span>ErrorCorrectingCodes</span></a> <a href="https://mathstodon.xyz/tags/LeechLattice" class="mention hashtag" rel="tag">#<span>LeechLattice</span></a> <a href="https://mathstodon.xyz/tags/LinearAlgebra" class="mention hashtag" rel="tag">#<span>LinearAlgebra</span></a> <a href="https://mathstodon.xyz/tags/Octonions" class="mention hashtag" rel="tag">#<span>Octonions</span></a> <a href="https://mathstodon.xyz/tags/GolayCode" class="mention hashtag" rel="tag">#<span>GolayCode</span></a> </p><p><a href="https://thmprover.wordpress.com/2025/01/09/from-error-correcting-codes-to-the-leech-lattice/" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">thmprover.wordpress.com/2025/0</span><span class="invisible">1/09/from-error-correcting-codes-to-the-leech-lattice/</span></a></p>