Alex Nelson<p>Another Thursday project idea for formalizing stuff in Mizar: The Icosians!</p><p>The Icosian group is isomorphic to the binary icosahedral group, but built out of quaternions.</p><p>We can use them to form a ring, also (confusingly) called the Icosians.</p><p>You can then form a lattice out of them, and it's isomorphic to the root lattice for the E8. It's really quite amazingly beautiful!</p><p><a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="tag">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/Quaternions" class="mention hashtag" rel="tag">#<span>Quaternions</span></a> <a href="https://mathstodon.xyz/tags/Icosians" class="mention hashtag" rel="tag">#<span>Icosians</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="tag">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/E8" class="mention hashtag" rel="tag">#<span>E8</span></a> <a href="https://mathstodon.xyz/tags/Lattice" class="mention hashtag" rel="tag">#<span>Lattice</span></a> </p><p><a href="https://thmprover.wordpress.com/2025/01/02/icosians-in-mizar/" 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/02/icosians-in-mizar/</span></a></p>