A home for Lean 4
libraries in development.
NYLL is the public development home for a growing collection of Lean 4 libraries. Work in progress is published here. As parts are completed, they are extracted and published as standalone libraries.
Published standalone libraries
These repositories publish parts extracted from NYLL. See each library for its scope, documentation, and source.
Pro-C Groups
Profinite and pro-C groups, free pro-C groups, and completed group algebras.
Class Field Theory
Local and global class field theory, reciprocity, and ramification.
Sawin’s Totally Real Towers
Sawin’s totally real tower theorem and related results of Martinet and Shafarevich.
Étale Fundamental Groups and Cohomology
Étale fundamental groups and étale cohomology.
Jacobian Varieties
Algebraic curves, Picard groups, and Jacobian varieties.
Research Papers
Formalizations of research papers.
Anabelian Geometry
Work toward the formalization of Grothendieck’s anabelian conjecture.
Authorship and verification
NYLL’s original code and documentation are Copyright (c) 2026 Naganori Yamaguchi. All original code developed for NYLL is written by OpenAI Codex. Source-specific credits and licenses are preserved for adapted and external material.
NYLL includes work in progress; publication here does not imply that every formalization is complete or verified. See the authorship, verification, and license details.