Formal Frontier

Formal Frontier publishes Lean libraries written by AI agents (“Formal Frontier Agents”, as their formalization.yaml files name the authors), with a dashboard at https://formalfrontier.github.io. This chapter maps the 44 libraries in trough's catalog, each read at a pinned commit: a part per subject and a section per library. A library's page quotes its formalization.yaml (its description, review and automation statements), links the Formal Frontier libraries it builds on and those that build on it, quotes the headline results of its README, and links a page listing the main results its formalization.yaml declares.

There are 267 articles: one for each highlight in a library's formalization.yaml whose declarations the scan finds (62), and one for each headline result in its README whose declaration link names a declaration that the scan finds in the linked file at the pinned commit (205). Of the 925 headline results, 497 link no declaration; 208 link a name the scan does not find in the linked file, 150 of them the file's module rather than a declaration; and 15 link a declaration that already has an article, which the library's page links in their place. The first two kinds have no article and stay as quoted text on the library's page. 17 libraries have no articles. The main results are not made articles: in several libraries they are close to the whole API.

No Lean is run for this chapter. Whether a file declares a name is read from its source text, following namespace, section and end; a name counts only when a declaration command in that file names it in full under the right namespace, so a name given relative to an open namespace, or one Lean generates (an additive version, a constructor), is left out rather than guessed, and so is a private declaration. Articles have no dependencies: edges between declarations need Lean. A declaration whose text in the file contains sorry is marked as stated without proof; a dependency on an unproved declaration elsewhere is not checked.

The quoted text is the libraries', under their Apache-2.0 license, with the repository and commit named where it is quoted.

The libraries

Each with its number of articles and the opening of its description, quoted from its formalization.yaml at its pinned commit, shortened with … where it is cut.

Commutative algebra

Adic modules (1 article): Lean theory of ideal-power torsion and adic module and ring completions, with quotient, tensor, finiteness and flatness interfaces. …
Algebraic direct limits (0 articles): Reusable Lean results for constant identity function and ring-homomorphism systems, varying-scalar directed limits, tensor products …
Coherent modules (76 articles): Coherent rings and modules, finite-presentation criteria, exact-sequence closure, localization and descent, coherent-module categories …
Finite étale algebras (0 articles): Finite etale subalgebra constructions over fields, spectrum component bounds over separably closed fields, and literal subalgebra …
Formal power series (0 articles): Integral weighted negative logarithmic derivatives of native formal-power-series units over arbitrary commutative rings, with group laws …
Graded rings (5 articles): Graded quotients and localizations, degree-multiplying maps of homogeneous localizations, homogeneous component surjectivity and polynomial …
Integral closure (7 articles): Integral-closure descent along linear retractions and normal-domain descent from arbitrary field scalar extensions of commutative algebras …
Minimal primes (30 articles): Classifies minimal primes over nonzero principal ideals in commutative semirings with unique factorization by normalized irreducible factor …
Multivariate polynomials (55 articles): Reusable multivariate-polynomial results on infinite-variable ideals, coordinate-difference evaluation ideals, polynomial maximal-spectrum …
Smooth regularity (0 articles): First-order conormal criteria and formally étale cotangent-space comparisons over commutative rings, presentation-relation and local …
Toric ideals (3 articles): Reusable Lean theory of coefficient-independent finite binomial kernels for monomial evaluation on finite variable types over arbitrary …

Ring theory

Group rings (1 article): Reusable Lean algebra equivalences from group algebras equipped with explicit free-abelian coordinates to multivariable Laurent polynomial …
Projective modules (7 articles): Row-finite linear systems with target satisfying Module.Baer have full solutions whenever every finite set of rows has a solution. …
Stable range (0 articles): Bass stable-range conditions for finite right-unimodular rows, quotient and local-ring consequences, regular and unit-regular rings …

Algebraic geometry

Algebraic groups (6 articles): Reusable Lean formalization of matrix point groups, finite algebraic group schemes and their coordinate algebras. …
Projective space (0 articles): Projective spectra of graded rings, polynomial standard charts and covers, homogeneous ideals, coordinate points, graded transport …
Ringed spaces (2 articles): Full ringed-space restriction, open-cover gluing and inverse-image factorization; …
Scheme properties (1 article): Reusable Lean theory of ring-valued point criteria, affine density, dimension bounds, single-cover subfunctor and group-object extensions …

Number theory

Dedekind ideal arithmetic (5 articles): Reusable ideal arithmetic, module indices and intrinsic heights of normed invertible modules over rings of integers. …
Iwasawa modules (1 article): Generic pseudo-null and directional pseudo-isomorphism calculus and the RingCat finite-quotient completed group algebra, topology …
Norm forms (0 articles): Field-norm/spectral-norm comparison over complete ultrametric fields; …
Polynomial root stability (4 articles): Fixed-degree stability of polynomial root-generated intermediate fields inside a common Krasner normed extension, including monic …
Quadratic algebras (0 articles): Quadratic-algebra presentations and total fraction rings, squarefree integral-closure criteria, diagonal quadratics, real-closed …
Valuation integers (5 articles): Power divisibility and a Krull-dimension bound for the integers of a rank-at-most-one valuation, a converse producing rank data from a …

Group theory

General linear groups (6 articles): Finite general linear groups over possibly noncommutative semirings and rings: …
Group theory (2 articles): For finite I and a commutative topological group E, ContinuousMonoidHom.intPiEvalEquiv I E identifies continuous homomorphisms from the …
Profinite groups (0 articles): Reusable Lean APIs for finite-stage limits, finite-target map colimits, maps into limits of finite-space diagrams, profinite-group …
Supernatural numbers (0 articles): Prime-exponent supernatural arithmetic, finite-quotient profinite orders and indices of closed subgroups, a closed-subgroup tower law, and …

Homological algebra and category theory

Continuous group cohomology (0 articles): Native continuous group cohomology in low degrees; …
Finite-group Tate cohomology (0 articles): Reusable Lean norms, exceptional Tate degrees, and objectwise additive cyclic period-two comparisons for finite-group representations.
Homological algebra (0 articles): Finite Euler sums for chain and cochain complexes, with native exact-sequence, exact-functor and shift results, plus fixed-arrow relative …
Morphism properties (0 articles): Relative preservation of maps between pullbacks, canonical transport between structured over-categories, pullback pairing over a fixed base …
Sheaf cohomology (0 articles): Compact-open filtered section colimits, quasi-flasque acyclicity, sheaf cohomology and right-derived pushforward, native sheafed-space …
Simplicial objects (0 articles): Functorial augmented left decalage of simplicial objects with a canonical extra degeneracy, and finite-fiber coproduct, diagram and …
Simplicial rings (0 articles): Central polynomial simplices over arbitrary unital rings, their coefficient-natural polynomial retraction and explicit algebraic simplicial …

Topology

Fundamental groupoids (6 articles): Endomorphism transport, chosen-vertex equivalences and connectedness of fundamental groupoids, with small-path generation and constructed …
Ideal completion (2 articles): Ideal completions of bounded distributive lattices: …
Metrization (3 articles): The Nagata–Smirnov sigma-locally-finite open-basis criterion and its metric converse, and metrizability from a locally finite closed …
Restricted-product duality (1 article): Compact finite-exceptional-stage control under T1 on a cofinite restricted product or openness of its distinguished subsets, singleton …
Spectral Stone duality (2 articles): Prime-ideal spectra of bounded distributive lattices and their contravariant equivalence with spectral spaces. …
Sphere topology (22 articles): Reusable Lean topology and singular homology: …
Vector bundles (5 articles): Compatible Hermitian and real fiber metrics on finite-dimensional vector bundles; …

Analysis

Complex analysis (7 articles): Complex Fréchet differentiability on open subsets of finite-dimensional complex normed spaces implies local analyticity for maps into …
Sequence growth (2 articles): Natural-division recurrence bounds and eventual exponential domination for sequences of natural numbers.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.