Skip to content

Trough

Trough maps Lean formalization libraries: what each one formalizes and how its results depend on one another, not what the library may add. Each library gets the article unit that suits it, such as curated concepts for Mathlib, the declarations its roadmaps name and the results its docstrings name for Tau Ceti, blueprint nodes for the research projects, headline results for Formal Frontier and project cards for Lean Pool. The maps are rendered with AutoformBot.

Chapters

  • Mathlib: One article per concept on Mathlib's four curated lists (overview, undergraduate, Freek's 100, 1000+) that Mathlib has, linked to its declarations, with edges collapsed from Mathlib's declaration graph.
  • Tau Ceti: One article per declaration a roadmap's status names as a result or notable definition, and per result Tau Ceti's docstrings name, the forms of one result together, as Tau Ceti has it: its docstring, signature and dependencies, in a part per top-level area with a section per roadmap or area of modules.
  • ATLAS (17,683 Lean files): Mapped separately: one article per documented public declaration, at https://deicyde.github.io/atlas-lean/.
  • Fermat's Last Theorem (Imperial): One article per node of its leanblueprint that is in Lean, with dependencies from its uses; the Verso blueprint (3 chapters) is left for later.
  • PNT+: One article per node of its LeanArchitect blueprint that is in Lean, with dependencies from its uses; the Blueprint build workflow builds the blueprint weekly with lake build :blueprint.
  • Polynomial Freiman-Ruzsa: One article per node of its leanblueprint that is in Lean, with dependencies from its uses.
  • Equational Theories: One article per node of its leanblueprint that is in Lean, with dependencies from its uses; the equations and implication classes in the project's data files are left for later.
  • Strong PNT (Math Inc): One article per node of its leanblueprint that is in Lean, with dependencies from its uses. The project gives no license, so the articles link to its statements rather than quote them.
  • Formal Conjectures: One article per problem file that states a research or textbook statement (1,814), on a page per source folder, with an index by AMS subject and the four FC100 lists; each statement's card says whether it is open, solved (with or without a proof elsewhere), a textbook result, or proved in the repository, and test and API statements are counted in their problem. Most statements are stated without a proof.
  • Fermat's Last Theorem (Anthropic): The 49 landmark theorems of its web pages, one article each in the route steps of PROOF-PATH.md, with the citation DAG between them.
  • Classification of Finite Simple Groups (Axiom): The proof as the repository writes it: the top theorem, the reduction to its cases and the theorem for each case, then one article per milestone module directly under CFSG/Milestones/, titled by Lean names: each declaration's Lean statement, or a definition's text, source line and status, read from the source without Lean. Edges from the top theorem's proof to the reduction and the cases, and from imports between case and milestone files; the formalization.yaml main results on the chapter's front page.
  • Lean Pool: One article per project card in LeanPool/projects, in a section per top-level MSC2020 class: the card's summary, authors, sources, provenance and license, and its main results' informal statements, each with its declaration where the scan finds it in the project's files.
  • Formal Frontier: 44 libraries, a part per subject. One article per highlight in a library's formalization.yaml whose declarations the scan finds, and per headline result in its README whose declaration link names a declaration the scan finds in the linked file; the main results its formalization.yaml lists are on a page of their own.

Libraries still to map

Libraries

  • Physlib (1,520 Lean files): One article per documented declaration, grouped by physics area; granularity to be checked against a docstring count.
  • CSLib (341 Lean files): One article per documented public declaration.
  • Foundation (320 Lean files): One article per documented declaration; the Zoo's inclusion diagrams between logics as edges.
  • Analysis I companion (109 Lean files): One article per textbook section (the Section_X_Y modules).

Large corpora

  • OpenAI Math (163,097 Lean files): One article per result family in CONTENTS.md, joined to the 208 formalization.yaml main results.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.