Lean 4 formalization of Langlands's First Main Lemma for local epsilon factors.
-
Updated
Sep 16, 2026 - Lean
#
langlands
Here are 5 public repositories matching this topic...
Statement-level Lean 4 formalisation of compatible families of λ-adic Galois representations and the companion-existence slice of Lafforgue's theorem, with an audit record.
-
Updated
Sep 5, 2026 - Lean
-
Updated
Feb 13, 2023 - SCSS
AI supporting the Langlands Program
-
Updated
Sep 5, 2026 - Python
The strong coupling constant α_s(M_Z) = Ω₄/23 = 0.117921 from the real period of elliptic curve 1132b1 divided by the discriminant prime of x³−x−1. Zero free parameters. 0.02% match to PDG.
qcd number-theory modular-forms arithmetic-geometry langlands loop-quantum-gravity fundamental-constants birch-swinnerton-dyer lmfdb pisot-numbers strong-coupling-constant alpha-s elliptical-curves gross-zagier elliptical-periods pisot-dimensional-theory
-
Updated
Apr 15, 2026 - Jupyter Notebook
Add this topic to your repo
To associate your repository with the langlands topic, visit your repo's landing page and select "manage topics."