LeanTrail

LeanTrail: A Visual Interface for Exploring and Auditing Mathematical Formalization Projects in Lean

LeanTrail connects papers, blueprints, Lean declarations, dependencies, and open work into a coordinated visual interface for inspecting formalization coverage item by item.

Abstract

Mathematical formalization projects in Lean bring together informal exposition, formalization plans, formal code, and dependencies between declarations. Although development environments support writing and checking code, they provide limited visibility into how the results of a paper are distributed across a repository, and which relationships remain partial, uncertain, or incomplete. We present LeanTrail, a visual interface for exploring and auditing the state of Lean formalization projects.

The tool constructs an intermediate representation from the paper, the repository, and, when available, the blueprint, connecting mathematical items, plan nodes, Lean declarations, dependencies, and incompleteness indicators. This structure supports coordinated views for navigating the project, tracking results from the paper, comparing planned statements and code, inspecting local graphs, and keeping the analysis grounded in the source code.

The central contribution is to make formalization coverage inspectable item by item, distinguishing Formalized, Statement only, Partial, Blueprint only, and Missing cases, each accompanied by candidate matches and diagnostics. We demonstrate the tool on real formalizations and discuss how this visual traceability supports onboarding, progress tracking, and gap review in Lean projects.

Figures from the paper

LeanTrail pipeline diagram
Figure 1: LeanTrail pipeline. The system receives a paper, a Lean repository, and, when available, a blueprint; extracts mathematical items, declarations, dependencies, proof status, and blueprint links; generates project summaries and Paper-Lean/Paper-Blueprint alignments; and exports an intermediate representation used by the interface for overview, coverage inspection, and source-level navigation.
LeanTrail project map and blueprint interface on APAP
Figure 2: LeanTrail interface on the APAP project, focusing on the Project map and Blueprint tabs. The structural navigator (A), project map (B), repository summary (C), Lean source panel (D), and blueprint view (E) operate as coordinated views. Together, they connect the repository structure, formal code, and blueprint branches, exposing both complete Lean proofs and pending statements.
LeanTrail paper tab in an APAP case study
Figure 3: The Paper tab in an APAP case study. The structural navigator lists extracted paper items (A); selected results are inspected in the paper context (B); Lean source snippets show the corresponding declarations and their proof status (C); the focus panel exposes retrieved candidates and diagnostic explanations (D); and the coverage table summarizes the relation between paper items, blueprint nodes, and Lean declarations (E).