三枝洋一先生による数理科学2024年7月号の『ガロア理論における双対性』を参考に、ガロア理論をLean4で形式化する。 あえてmathlibを使わず実装した後、mathlibを使うとどうなるかをみる予定。 blueprint https://unaoya.github.io/lean_Galois/blueprint/ YouTubeで毎週土曜夜に配信予定 https://youtube.com/live/kr7U8XPmBJU?feature=share