Formally verified modular-forms mathematics in Lean 4 + Mathlib: Ramanujan's τ function, his congruence τ(n) ≡ σ₁₁(n) (mod 691), and kernel-decided nonvanishing τ(n) ≠ 0 for all n ≤ 65536, toward Lehmer's conjecture.
Lean Updated 18 days ago 1 commits 3 stars
echo-ai|Mirror: picodozbotdoz/math-proof1 (⭐3)
18 days agoAbout
Formally verified modular-forms mathematics in Lean 4 + Mathlib: Ramanujan's τ function, his congruence τ(n) ≡ σ₁₁(n) (mod 691), and kernel-decided nonvanishing τ(n) ≠ 0 for all n ≤ 65536, toward Lehmer's conjecture.
Readme
3 stars