Proof Atlas: geometric language for formal proofs

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.

Scientific questions

  1. Can a fixed vocabulary of visual primitives represent Lean’s kernel expressions and their binding, type and declaration relationships compositionally?
  2. Which abstractions reduce visual complexity while preserving explicit boundaries, assumptions and recoverability of the underlying formal terms?
  3. Does the same language work for small human-written examples and very large machine-generated proofs, without drawing or expanding every occurrence?
  4. 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

Research layers

  1. Kernel vocabulary: the twelve version-pinned Expr constructors, universe levels, ordered ports and scope/reference links.
  2. Structural composition: occurrence-aware scenes, sharing, exact cuts, navigation and reversible expansion against an immutable packet.
  3. Proof structure: recognizable introduction/elimination constructions, complete applications, hypotheses and conclusions. Classification must use checked term/type information rather than attractive labels.
  4. Semantic abstraction: reusable modules and mathematical interpretations with stated assumptions and independently checked correspondence where available.
  5. Source and elaboration: surface syntax, tactics, commands, macros and elaborator traces, attached through explicit provenance. Kernel expressions do not reconstruct missing tactic histories.
  6. 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.

First implementation milestone: an article-independent, budgeted geometric scene representation with ordered ports, exact occurrence paths, lexical-scope links and complete frontier accounting, tested on small adversarial examples and both compiled inventories. This milestone is part of the program, not its completion.

First structural implementation

The optional scoped geometry prototype is independent of the article map. Its versioned scene contract retains all twelve kernel constructor kinds, ordered child ports, occurrence-qualified vertices, lexical-scope links and exact collapsed boundaries. Universe and other constructor payloads remain attached; they are not yet a complete geometric notation of their own.

A scene is a finite cut of the expanded occurrence tree, constructed directly from the shared packet. Each displayed occurrence contributes one; a frontier contributes the number of descendants hidden below it. Their sum must equal the selected root’s exact expanded count. External binder targets remain explicit context boundaries. domain is the exporter’s display alias for Lean’s binderType; the scene records both port names. The cut is recoverable against its packet, not a standalone proof certificate.

The audit currently checks 6,166 cuts across all 2,098 packets and 4,972 lexical-scope links. Three synthetic scope controls include a shared bound-variable node with different binders, a let value outside its new binder and an enclosing binder outside the current cut. These controls are structural tests, not additional kernel certificates.

In the real JacobiCore.E_pos proof, shared node 17 appears on two displayed routes and points to different binders. The prototype draws separate occurrences. The initial largest proof-body cut shows 9 occurrences and records 462,476,262 hidden descendants, accounting for 462,476,271 body occurrences. This verifies the cut’s accounting, not meaningful semantic compression or human comprehension. The raw depth cut can stop in a binder telescope before exposing the mathematical argument; the optional abstraction below addresses this specific obstruction.

Reproduce with node scripts/test-proof-atlas-geometry-core.cjs; after the production site build, run node scripts/test-proof-atlas-geometry-browser.cjs. The browser checks real canvas/keyboard selections, distinct scope targets, exact boundary refinement, saved routes and the large body at phone/desktop widths in both themes.

Scene implementation · Independent path/scope audit · Browser checks

Binder-telescope abstraction

The optional Fold binder contexts rule contracts a contiguous prefix of lam, forallE and letE along their body ports. Tₙ denotes an ordered n-entry telescope, not an additional Lean constructor. Mixed prefixes retain each entry’s constructor, payload, visibility and original route. Type/domain and let-value regions remain separate hidden regions in the environment before their own binder. The continuation uses the environment after all retained entries.

ProofAtlasGeometricScene/2 distinguishes drawn vertices from retained kernel occurrences. A telescope with n entries retains n binder occurrences and the exact roots of its header regions. Thus retained binder occurrences + hidden header regions + continuation = original subtree, using exact expanded counts. No represented term is rewritten. Ordinary scene version 1 remains available by turning folding off.

References from the displayed continuation to a folded binder keep the original target path plus a telescope vertex and one-based slot. The ordered header list opens the exact binder, its type or let-value region. The continuation also has an exact navigation link. A prefix scan is capped at 64 entries per compound node; a longer prefix is explicitly marked as continuing, rather than silently omitted.

The independent audit checks 4,164 folded cuts across all 2,098 packets: 3,545 telescope vertices, 17,978 retained binder entries and 3,260 displayed links to folded slots. Small adversarial controls check a mixed lambda/forall/let prefix, shadowing, dependent header scopes, exact partition of every original occurrence and a deliberately truncated prefix. Five corruption/limit controls must be rejected. These are representation checks, not a semantic proof-compression certificate.

On the largest compiled proof body, the 13-entry prefix becomes one vertex and the first non-binder application is exposed. The resulting initial view has 14 vertices retaining 26 kernel occurrences plus 462,476,245 hidden occurrences, still accounting for the original 462,476,271. This improves access past the header; readability of the remaining application structure and human comprehension remain unmeasured.

Folded example · Large proof example · Telescope audit · Browser checks

Application-spine composition

The optional Group applications rule gives a left-associated chain (((h a₁) a₂) … aₙ) the representation @ₙ(h; a₁, …, aₙ). It retains all n original Expr.app occurrences, the exact head route and the arguments in call order. Its accounting identity is n + size(head) + sum(size(argument)) = size(original). No beta reduction, implicit-argument omission or term rewriting occurs. The rule composes with the telescope rule; application ports do not introduce binders.

head and argN are explicitly abstract ports, rather than invented kernel fields. A head need not be a constant. The rule stops at lambdas, projections, metadata and other non-application constructors. A selected inner application represents that selected term only; it does not acquire arguments from enclosing applications. A complete function spine does not establish that a call is saturated, that an argument is a proof or that an arrow is logical inference. Those require additional type evidence.

Scene version 3 has separate bounds for drawn vertices, depth, ports per application and vertices per layer. The initial view draws at most 48 term vertices, four levels below the selected root, six ports per compound application and eight term vertices per layer. Undrawn head/argument regions retain their complete roots, routes and occurrence counts. All grouped arguments, including undrawn ones, have navigation controls. Explicit enclosing-context boundary vertices are additional to the term-vertex budget. A function-spine scan is capped at 64 applications; if that limit is reached, the remaining function spine is retained as a region and the visible arguments have relative trailing-slot numbers, not fabricated absolute positions.

Across all 2,098 packets, the audit checks 4,164 composed cuts containing 18,787 application groups, 70,347 retained applications and 8,641 lexical-scope links. Independent controls cover nonconstant heads, metadata boundaries, shared variables under argument binders, selected inner applications, capped spines, complete small-term occurrence partitions, node/depth/layer limits and eight rejection cases. These establish serialized structural correspondence, not new kernel certificates.

For SBracket.mk.inj, a 57-entry telescope leads to a 59-argument application of SBracket.mk.noConfusion. The view exposes the head and first five arguments; the 59th argument remains directly selectable at its original route. On the largest body, the composed initial cut has 21 vertices retaining 70 kernel occurrences plus 462,476,201 hidden occurrences, accounting for the original 462,476,271. These bounds describe a recoverable view, not a measured improvement in human comprehension.

Composed example · 59-argument example · Application audit · Browser checks

Checked occurrence types

The first type layer attaches native Lean judgments to exact occurrence routes. It does not classify arguments from constructor tags or declaration names. Before checking a selected term, the extractor compares the native declaration’s complete shared DAG—constructors, payloads, ordered fields, roots, counts and scope requirements—with its published packet. The private extraction driver also verifies the source module hash, compiler version and pinned revisions of compiled dependencies on the search path. Packages pinned in the manifest but absent from that path are recorded separately.

For each route, the extractor reconstructs its lexical context with Lean local and let declarations. Domains and let values use the pre-binder context; bodies use the extended context. Each introduced domain is checked to be a type, and each let value is checked against its declared type before extending the context. The kernel then checks the selected expression in that well-formed context. Argument domains are instantiated in call order, compared with argument types, and checked after substitution into the result type. An argument is labelled proof when its checked type is a proposition, type when that type reduces to a sort, and value otherwise. Binder visibility is recorded separately. These categories do not assert call saturation or turn an application edge into a logical implication.

Each judgment retains a shared type-expression DAG with its context abstracted back to bound indices. Reopening that type in its original context must reproduce the inferred expression by structural equality, including binder names and metadata. Pretty text is a presentation, not the formal type. The browser checks the sidecar hash, packet identity, exact route, complete enclosing-binder list, argument order and type-graph scope. The browser does not rerun Lean. These are native extraction attestations tied to the recorded environment, not portable kernel certificates or certified article equivalences.

The primary query inventory contains 943 selected occurrence judgments in five declarations, with 2,784 argument observations. It covers finite geometry-derived queries for JacobiCore.E_pos, JacobiData.slope_bound_abs, SBracket.mk.inj and CrossingData.crossing in the published snapshot, plus JacobiConcrete.AmplitudeChart.midpoint_polynomial in the working snapshot. This is not complete occurrence-type coverage of those proofs or the 2,098-packet inventory. A path without a primary query or an explicit application-trace observation remains without recorded type evidence; it does not inherit a judgment from a shared node or enclosing match.

The data audit checks 146 shared nodes appearing in distinct recorded contexts and rejects 37 altered-hash, stale-packet, wrong-node, wrong-context, changed-count, duplicate-route, reordered-argument, missing-environment and unreviewed source-syntax cases. Small independently run native controls check proof/type/value roles, dependent contexts and let scope. Two deliberately ill-formed surrounding contexts must be rejected; changing a serialized binder name also makes the native/packet comparison fail. The browser exercises exact argument and type selections, statement/proof distinction, missing-path fallback, rejected evidence without losing the original graph, and article synchronization.

This adds typed argument labels and a selected-term typing judgment to the structural geometry. The initial type-expression notation below reuses its constructor rules. Logical introduction/elimination diagrams, broader type coverage and measured proof-inspection tasks remain open work. The blog has no new result claim for this implementation.

Typed example · Type attachment audit · Native controls · Browser checks

Type-expression geometry and structural sharing

Show type diagram draws a recorded type using the same constructor shapes, ordered ports, binder telescopes and application spines as the proof view. A type component is either the selected expression’s type, an argument’s actual type or the corresponding instantiated expected domain. Every component identifies its native judgment route, type-evidence hash and root in the shared type table. This is a structural diagram of a recorded type; selecting a descendant does not produce an additional inferred typing judgment.

Scene version 4 separates two binding namespaces. A type-local bound variable points to its exact binder within the type expression. A variable bound by the original proof context points to an explicit Γ boundary with that original proof occurrence’s route. Type-local navigation refines the type view; selecting Γ returns to the original proof binder. Binder domains and let values continue to use their pre-binder context. The article selection remains unchanged during type-local navigation. An argument component also provides a direct link to its original proof occurrence.

The initial type cut is bounded by 32 term vertices, depth three, six term vertices per layer and four displayed application children; context boundaries are additional. Hidden regions retain exact counts and navigation controls, including all arguments of a grouped application. The same type may have different meanings under different contexts; neither a shared type-node identifier nor visual similarity identifies those meanings.

The serialized format interns repeated type expressions within each declaration, preserving every constructor payload, ordered child, expanded count and scope requirement. The initial type-only projection contained 25,840 shared nodes instead of 144,470 separately serialized nodes, with five compressed files totalling 339,688 bytes instead of 1,232,961. The richer application projection below extends these tables. The publisher compares the original and packed contextual judgments using recursively hashed structural roots, then the audit recomputes that fingerprint. This is lossless structural packing, not definitional equality, semantic compression or a new kernel certificate.

The audit checks all 6,511 initial component cuts, including 1,359 displayed links to original proof binders and 212 to type-local binders. It independently resolves displayed bound variables, checks exact retained/hidden accounting and rejects 20 modified scene controls. A synthetic open-expression control separates an ambient proof binder from an internal type binder; it is a structural test. The sharing audit rejects 15 changed-context, changed-role and changed-payload controls. Browser tests exercise actual canvas and keyboard jumps, component selection, pre-binder domains, source changes, unsupported article selections and accessibility at phone and desktop widths in both themes.

This extends the common syntax/binding notation to the selected recorded types. It does not supply logical inference rules, complete type coverage, an AI-generated corpus benchmark or measured comprehension results. The broader program remains active.

Type geometry audit · Sharing audit · Browser checks

Checked Π-application rule

Show application judgment displays one argument stage as a typing rule. It separates this checked relation from the structural graph’s child arrows:

Γ ⊢ f : τ       τ ≡ Π (x : A), B
Γ ⊢ a : A′      A′ ≡ A
──────────────────────────────── Π application
Γ ⊢ f a : τ′    τ′ ≡ B[a/x]

The function premise, argument premise and conclusion retain their original compiled occurrence routes and share the same enclosing context Γ. Type links open the existing constructor geometry for τ, its normalized Π expression, A′, A, τ′ and the substituted result B[a/x]. Selecting a term returns to its original proof occurrence. Stage navigation refines the rule without changing the selected proof or article. A type load from an earlier stage cannot restore that stale selection.

Native extraction kernel-checks the head, each argument and each application prefix. It records the function type before normalization, the Π expression, actual and expected argument types, and both inferred and substituted result types. Conversion is checked by asking the kernel to type-check a typed identity applied to the term at the proposed type. Thus the function-to-Π, argument-to-domain and result-to-substitution checks do not rely on the browser or on Meta.isDefEq alone. Every recorded type still passes abstraction/reopening equality in the original context. These are recorded native checks, not portable kernel certificates.

All 399 applications among the primary queries have complete traces: 2,784 argument stages and 8,352 kernel conversion checks. The longest trace has 59 stages. In 2,268 stages the Π body syntactically contains its current bound variable; this does not measure semantic proof dependence. The corpus queries all have constant heads. Seven fresh small native control applications separately test function-variable heads, dependent substitution, definitionally equal but structurally different domains, let scope and a partial application returning a function. Four of those controls have nonconstant heads. An invalid typed conversion is rejected.

The traces also supply 754 additional exact type observations, yielding 1,697 typed occurrence routes in these five declarations. An observation is an explicitly recorded head, application prefix or argument, with its source query and stage retained. Primary queries and these observations remain distinguishable. All overlapping observations agree structurally on type, role and context. No type is assigned from an arbitrary ancestor or from a shared node identifier. An argument observed as a term does not acquire an invented trace for its own internal arguments.

Complete traces have a fixed allowance of 32,768 shared type nodes per primary judgment; ordinary judgments retain their 8,192-node allowance. The packed declaration table is bounded by 65,536 nodes, and each displayed type cut still uses at most 32 term vertices. The initial 8,192-node trace allowance withheld 33 cases. Retrying those exact routes with the larger fixed allowance resolved all 33; the largest observed table used 13,879 nodes. The merge requires identical packet/environment headers and unchanged contextual core judgments. All 943 original core judgments were independently compared with the preceding release and remain unchanged.

The richer projection has 26,795 shared type nodes instead of 622,744 separately serialized nodes and occupies 844,759 compressed bytes instead of 4,088,554 without interning. The application audit checks all 2,784 rule stages, 16,704 linked type-component cuts, 754 observation cuts and 80 rejection controls. Fresh native controls additionally exercise the visual model and reject changed-context/environment merges. Browser checks cover premise/conclusion and Γ jumps, observation provenance, the 59-stage trace, delayed loads, missing optional code, unsupported article selections and keyboard/accessibility behavior in both themes and viewport sizes.

This supplies one compositional typing rule. It does not yet provide lambda-introduction or recursor-elimination diagrams, inventory-wide type coverage, an AI-origin benchmark, measured comprehension results or shareable stage/type-local selections. The general research goal remains active; the blog is unchanged.

Application rule model · Application audit · Fresh native model controls · Browser checks