Proof Atlas research program

Status: active research program. Established 15 October 2026 by the repository owner.

Goal

Develop a consistent, compositional geometric language that transforms Lean proofs into faithful, navigable visual representations, including massive proofs generated by AI. The language should let a person inspect assumptions, binding, constructions, lemma applications and proof structure at several scales, while retaining access to the original formal object. Visual proof construction with Lean checking is a longer-term objective.

The article reader is an application and evaluation case. Improving an article, drawing a theorem-specific diagram or completing a deployment does not complete this research goal.

Reading route

Learn the notation. Constructor fields, scope references, folded regions and typing rules, with four interactive examples.
Inspect a recorded proof. Use the Riccati bound as a worked case. Every selected source object keeps its exact compiled route.
Check the evidence. A searchable index organized by kernel notation, scoped composition, typing, context interfaces and evaluation.

The SE(2) article reader is a separate application. The published structural result reports the corpus and article-coverage findings; it is not this program’s navigation index.

Current position

Layer	Supported capability	Remaining question
Kernel vocabulary	Twelve constructor forms, ordered fields, levels and lexical references.	How should richer payloads be presented consistently?
Scoped composition	Exact cuts, reversible telescopes/application spines and shared storage.	How broadly can paged delivery be provided without expanding the occurrence tree?
Typed constructions	Recorded applications, introductions, local definitions and selected elimination cases.	A general readable notation for arbitrary elimination remains incomplete.
Context interfaces	Original binder/use links, explicit boundaries and recorded native context observations.	Syntactic support is distinct from mathematical premise necessity.
Semantic abstraction and evaluation	Finite structural and native checks, including a separately attributed AI-source sample.	Semantic compression and improved human comprehension remain unmeasured.

Scientific questions

Can a fixed vocabulary of visual primitives represent Lean’s kernel expressions and their binding, type and declaration relationships compositionally?
Which abstractions reduce visual complexity while preserving explicit boundaries, assumptions and recoverability of the underlying formal terms?
Does the same language work for small human-written examples and very large machine-generated proofs, without drawing or expanding every occurrence?
Does the representation improve proof inspection, error localization and navigation? These require measured user tasks; graph size and browser checks alone do not answer them.

Required invariants

A visible source object identifies its compiled packet and exact occurrence route. A computed object identifies its checked derivation record, separate namespace and exact path within the computed graph; it never acquires an invented source occurrence. A shared DAG node identifier alone is insufficient for binder meaning.
Constructor ports retain their names, order and roles. Function/argument, binder domain/body, let type/value/body and projection structure are distinct.
Bound-variable links follow lexical scope. Binder domains and let values do not acquire the new binder; bodies do. A link outside the current view remains an explicit context boundary.
Universe levels, declaration references, metadata and unresolved elaborator objects have distinct representations. Unknown context or inferred types are marked unavailable, never invented.
A collapsed boundary retains its exact root route and recoverable packet reference. Its represented occurrence count is exact; displayed and hidden structure must account for the complete selected region.
Types, proposition expressions and proof terms remain distinct. A constructor or lemma reference does not by itself establish a logical implication or mathematical explanation.
Positions, distances and colors are presentation choices unless a specific invariant has been defined and tested. Visual similarity is not mathematical equivalence.
Every abstraction states whether it preserves syntax, checked typing, definitional equality or a separately reviewed semantic relation. These are different guarantees.

Research layers

Kernel vocabulary: the twelve version-pinned Expr constructors, universe levels, ordered ports and scope/reference links.
Structural composition: occurrence-aware scenes, sharing, exact cuts, navigation and reversible expansion against an immutable packet.
Proof structure: recognizable introduction/elimination constructions, complete applications, hypotheses and conclusions. Classification must use checked term/type information rather than attractive labels.
Semantic abstraction: reusable modules and mathematical interpretations with stated assumptions and independently checked correspondence where available.
Source and elaboration: surface syntax, tactics, commands, macros and elaborator traces, attached through explicit provenance. Kernel expressions do not reconstruct missing tactic histories.
Applications: article correspondence, proof auditing, generated-proof inspection and eventually visually constructed proofs checked by Lean.

Evaluation and evidence

Use synthetic adversarial controls, small kernel-checked examples, the published compiled corpus and its separately labelled working snapshot. Include shared terms used under different binders, shadowing, dependent domains, let bindings, projections, universe parameters, open contexts and extreme expansion ratios.

For large proofs record input packet hashes, displayed occurrence budget, frontier accounting, scope-link checks and bounded-memory traversal. Current large packets are scale tests; do not label them an AI-generated benchmark without recorded generation provenance. Add diverse independently sourced and AI-generated proofs when their provenance and publication rights are established.

Public packet checks establish serialized structural correspondence. Independent kernel replay, visual-language adequacy, semantic compression and human comprehension require their own evidence. The existing constructor catalogue and article-specific diagrams are useful foundations, not a completed general language.

Working rule

Prioritize general language rules and falsifiable tests over article-specific styling. Each iteration should identify a representation problem, implement or reject a rule, and retain its evidence and limitations. Keep the program active across application releases. Publish only significant supported positive or negative scientific results in the blog; keep routine software checks and operational records in technical evidence.

Current priorities: extend the compositional notation for elimination, broaden bounded source delivery and define measured tasks for tracing assumptions, finding premises and localizing errors. A release is one test of the language, not completion of the program.

Technical evidence

The implementation record is available in the searchable evidence index. Earlier links to individual rules continue to open their original sections there.

Earlier section links