Showcase

Showcase is a tool for presenting formal Lean proofs: it turns a repository of Lean declarations into a browsable, self-contained site where every result sits beside its informal statement, its dependencies, and the evidence for believing it.

It is agnostic about where the Lean came from. A hand-written blueprint developed alongside its prose and a machine-generated corpus of twenty-five thousand declarations get the same treatment, and the second case is the one that shaped the design: at that scale nobody reads the repository, so the presentation layer is the interface, and its trust claims have to survive scrutiny they were never going to receive by hand.

That commitment runs through the whole tool. The site distinguishes, visibly and per item, between what a machine checked and what a person asserted — a build-time Lean.collectAxioms audit over every presented declaration, structural gates on the dependency graph run before any HTML is written, per-block markers recording how each piece of code was rendered, and a "Trust model" page stating plainly what none of that covers. Claims contradicted by the environment fail the build rather than rendering as green badges.

A Showcase project combines:

informal mathematical exposition beside each formal declaration
links to local Lean code or existing Lean declarations
optional attached Rust code blocks on labeled nodes for mixed-language notes
optional external TeX or Markdown markup attachments on labeled nodes to help port existing documents
automatic tracking of formalization progress by analyzing the associated Lean code and declarations, including incomplete declarations such as sorry
a build-time kernel axiom audit, checked against the project's declared claims
rendered overview pages such as dependency graphs and progress summaries
HTML output with previews, navigation, and exported metadata

Naming. "Showcase" is the product name, and the GitHub repository is eric-vergo/Showcase (canonical). The Lake package is still VersoBlueprint, the directives are still blueprint_*, and the option namespace is still verso.blueprint.* — renaming those would break every consumer for no benefit. Expect the code to say "blueprint" and the site to say "Showcase". Older docs or dependency pins may still spell the repository eric-vergo/verso-blueprint; use eric-vergo/Showcase.

Provenance & authorship

This is a fork, not upstream, and its files carry two layers of authorship. Upstream-lineage files (derived from leanprover/verso-blueprint v4.32.0, by Lean FRO, LLC and contributors including Emilio J. Gallego Arias and David Thrane Christiansen) keep their original copyright and author(s), with the fork's contributors appended where the fork modified them. Fork-original files (created here, with no upstream counterpart) are Copyright (c) 2026 Eric Vergo, authored by Eric Vergo with AI assistance from Anthropic's Claude models — Claude Fable 5 and Claude Opus 4.8, per the git commit trailers, the record of which model did what. See NOTICE for the full layered story; scripts/check-header-provenance.sh guards against fork-original files silently reacquiring the upstream header template.

What this fork changes vs upstream

This is eric-vergo/Showcase, a fork of leanprover/verso-blueprint that turns the Blueprint genre into a browsable, self-contained presentation layer for formal proofs. It is the genre powering the A362583 irrationality showcase — https://eric-vergo.github.io/OEIS-A362583-Irrationality/.

The fork's feature program, layered over upstream's genre:

Per-node & per-declaration pages. Every blueprint node gets its own page (slug routing with Greek-letter transliteration) with a side-by-side informal ↔ Lean card (proof bodies hidden by default), plus per-declaration pages, short display names, and declaration index / catalog pages.
Dependency graph, dashboard & project-management hub. A transitive-reduction dependency graph (show-all-edges toggle, all-declarations mode, essential view, status filter, dark-mode framed cards) drawn with self-hosted d3 / d3-graphviz; a landing dashboard with self-hosted d3 charts; and a single "Project management" top-nav feeding a pm/ hub (worklist, owners, tags, audit, Mathlib candidates, definitions, theorems, modules, index).
Trust surfaces that fail closed. A claim-first comparator page (verdict, scope, the certified statement verbatim, reproduce commands pinned to what CI actually ran), a formalization.yaml metadata page, a Trust model page separating machine-checked from author-asserted, and a build-time axiom audit (Lean.collectAxioms over every wired and project declaration) whose findings contradict-check the project's own formalization.yaml and fail the build when they disagree. Structural uses-graph gates (acyclicity, unresolved labels, optional connectivity) run between traversal and emission, so a failing gate leaves no site on disk. Configured through verso.blueprint.trust.* / declNamePrefix / graph.includeAllDecls / math.lint / externalCode.strictResolve lakefile options.
Verbatim-source signatures & marked rendering tiers. Node signatures are the author's verbatim source, re-elaborated in the declaration's own namespace (with a delaborated fallback); proof bodies render without inline proof-state toggles so per-token type hovers work; build-time TikZ → SVG offline figures. Every code block carries a corner marker recording which pipeline produced it, so a silent fallback from "re-elaborated and checked" to "coloured text" is visible to the reader.
Full light/dark theming. Everything themes via data-bp-color-scheme with the --bp-color-* / --bp-space-* / --bp-duration-* / --bp-fs-* token scales, a restrained dev-tool-docs visual identity, and offline / self-contained emitted output (no CDN or off-origin assets in the generated site).

Wiring

The fork pins its own upstream forks from git so it resolves standalone and for published consumers:

verso → git eric-vergo/verso @ blueprint (Verso fork that self-hosts marked for strict-CSP / offline viewing; v4.32-based)
subverso → git eric-vergo/subverso @ blueprint (SubVerso fork for VSCode-faithful semantic highlighting: const type/function split + bracket-pair depth; classification only, no colors/HTML)
verso-slides → leanprover/verso-slides @ v4.32.0, proofwidgets → ProofWidgets4 @ v0.0.104
toolchain leanprover/lean4:v4.32.0

Branch layout

blueprint — the fork's work branch (default). Rebased onto upstream v4.32.0.
Upstream release branches (v4.28.0 … v4.32.0) are retained for reference and to track upstream.

Fork status: upstream capabilities not carried over

Because upstream v4.32.0 and this fork independently rewrote the shared graph / preview / manifest subsystem (upstream added a GraphModel/GraphData split and a strict PreviewKey type; the fork kept a combined GraphData with String preview keys under a large feature layer), the fork's src/ is carried as a coherent unit adapted to build on v4.32 Verso. Upstream v4.32 preview/graph capabilities that are inseparable from that replaced subsystem are not carried over. This section is the single source for those absences; nothing else in the documentation should describe them as available.

TeX and PDF export. Upstream only. This fork emits HTML and nothing else: there is no --pdf, no --pdf-engine, and no TeX writer. vbp build accepts exactly --output, --serve, and --port, and rejects anything else.
The external-markup fragment renderer. The metadata half of external markup is retained — see Math, TeX, and external markup for the implemented contract — but the generated HTML-cache fragment bodies, the --external-markup-render switch, and the Informal.ExternalMarkupView / Informal/ExternalMarkupRender.lean / PreviewManifest/Cli.lean modules that produced them are deleted relative to upstream.
Foreign-LSP references, and the standalone-slide + source-metadata runtime.

Start Here

Start a project

If you want to start a Showcase project today, start here:

project_template/README.md
doc/GETTING_STARTED.md
doc/MANUAL.md
doc/API.md when you need documented Lean, generated-data, or browser integration APIs; start with Choosing an API

To copy the starter and build its rendered output before renaming the package and modules:

cp -R project_template my-blueprint
cd my-blueprint
lake exe vbp build

This uses the checked-in Lake manifest and writes the HTML site under _out/site/html-multi/. To preview the site locally, run lake exe vbp build --serve. After that, follow the template README to rename ProjectTemplate to your project name and replace the starter chapters.

After building, query the generated planning data through vbp rather than reading generated JSON files directly:

lake exe vbp query work-queue
lake exe vbp query metadata

See real examples

For larger Blueprints in use, see Reference Blueprints.

Current Project Shape

Today a Blueprint project usually owns three things:

chapter modules containing the mathematical content
a Blueprint top-level file that assembles chapters and rendered overview pages
a generator entry point that resolves forward references, computes metadata, and writes the generated output under _out/

verso-blueprint provides the Blueprint directives, rendering commands, preview runtime, and support library code. The starter layout in project_template/ shows the recommended shape. For the broader rendered artifact index, including published reference blueprints and local test fixtures, see the published rendered artifact index.

lake exe vbp build writes the HTML site under _out/site/html-multi/. Its whole option surface is --output <dir>, --serve, and --port <n>; run lake exe vbp --help for the local synopsis. HTML is the only output this fork produces — TeX and PDF export are upstream capabilities it does not carry (see Fork status).

Three-Level Blueprint Model

Blueprint keeps three related layers separate:

Original sources and provenance. These are the papers, PDFs, imported files, page references, and source spans that explain where the mathematical content came from.
Informal Blueprint content. This is the labeled mathematical statement, proof, or definition as Blueprint understands it. Native Verso bodies are the normal representation. Raw Markdown or TeX external markup can also be attached to a labeled node as a compatibility representation while porting an existing document.
Formal Lean content. This is the Lean code or declarations associated with a Blueprint label. It drives progress state, declaration panels, and links between the informal document and the formalization.

A single Blueprint node can have data from all three layers at once. For example, a theorem can cite a source span in a PDF, keep a Markdown witness or native Verso statement as its informal content, and link to one or more Lean declarations. External Markdown and TeX attachments should be read as Level 2 informal content unless they are separately referenced by Level 1 source provenance metadata.

Core Features

Labeled nodes and rich directives

Every Blueprint node is identified by a label such as addition_spec or addition_right_identity. Those labels drive cross-references, graph nodes, summary entries, code associations, external-markup associations, and metadata export.

When roles such as {uses "foo"}[] or citations have an empty payload, Blueprint can automatically render text such as Theorem N. Metadata-only dependencies can be written on a block with (uses := "foo, bar"); inline and metadata-only uses can also carry intent tags such as "regular", "technical", or "auxiliary", plus an origin of "manual" or "automatic". Statement and proof directives render separate uses chips, so proof-only prerequisites can stay attached to the proof header without being folded into the statement chip.

Typical directives look like:

:::definition "addition_spec" (lean := "Nat.add, Nat.succ")
:::theorem "addition_right_identity" (owner := "jason") (priority := "high")
:::proof "addition_right_identity"

:::definition "addition_spec" (lean := "Nat.add, Nat.succ")
We write $`a + b` for the result of adding $`b` to $`a`.
:::

:::theorem "addition_right_identity" (owner := "jason") (priority := "high")
For every natural number $`n`, adding zero on the right leaves it unchanged:
$`n + 0 = n`.
:::

```lean "addition_right_identity"
theorem nat_add_zero_right (n : Nat) : n + 0 = n := by
  simp
```

Connecting to Lean

Blueprint supports three main ways to connect informal nodes to Lean:

inline code with a labeled Lean code block
compiled code tagged with @[blueprint "addition_right_identity"]
existing declarations referenced with (lean := "Nat.add_assoc")

@[blueprint "addition_right_identity"]
theorem nat_add_zero_right (n : Nat) : n + 0 = n := by
  simp

Add (autoDeps := true) when a tagged declaration, labeled inline Lean block, or (lean := "...") statement should infer statement/proof dependency edges to directly referenced Lean declarations that are already associated with Blueprint labels. You can also set set_option verso.blueprint.autoDeps true for a file or section, with local (autoDeps := false) available as an override. Inferred edges are recorded with origin "automatic"; explicit uses and proofUses entries remain manual unless written through the usual Blueprint dependency syntax. Manual {uses ...} links remain available for prose-first Blueprint nodes.

:::theorem "addition_assoc" (lean := "Nat.add_assoc, Nat.add_comm")
This informal node is linked to existing compiled Lean declarations.
:::

Attached Rust code

Blueprint also supports labeled inline Rust code blocks:

:::definition "ffi_helper"
Helper routine mirrored in Rust.
:::

```rust "ffi_helper"
pub fn ffi_helper(x: i32) -> i32 {
    x + 1
}
```

Current behavior:

the Rust block attaches to the Blueprint node with the same label
the rendered page shows an associated Rust code panel
rendering uses a small built-in syntax highlighter
Rust blocks do not currently affect Blueprint progress/status semantics
Rust diagnostics and external Rust references are not part of the current surface

Math, TeX, and external markup

Blueprint supports inline math such as $`n + 0 = n` and display math such as $$`\sum_{i=0}^{n} i = \frac{n(n+1)}{2}` . It also supports TeX preludes via tex_prelude and best-effort KaTeX linting during elaboration. KaTeX is the renderer used by the generated HTML.

Blueprint nodes can also carry raw external markup through labeled tex and md code blocks. These blocks are Level 2 informal representations in the model above, not original-source provenance by themselves:

:::theorem "addition_right_identity"
For every natural number $`n`, $`n + 0 = n`.
:::

```tex "addition_right_identity"
\begin{theorem}\label{thm:addition-right-identity}
For every natural number $n$, adding zero on the right leaves it unchanged.
\end{theorem}
```

```md "addition_right_identity" (slot := proof)
This was imported from a Markdown proof sketch.
```

Labeled standalone tex and md blocks are exported as semantic external-markup catalog entries. What survives the fork is the metadata half: the attachment is stored on the labeled node and exported in the Blueprint manifest, either as its own externalMarkup:<label> entry (for a label with no rendered Blueprint statement or proof) or folded into that label's block entry (when there is one). Bodyless Blueprint directives that carry (lean := ...) still contribute their Lean preview keys and code data to the exported manifest entry; the generator warns if that metadata is ever dropped during manifest export.

Display at the code-block location is controlled entirely from Lean, not the command line. The default is hidden; set set_option verso.blueprint.externalMarkup.display "summary" (a metadata summary) or "source" (escaped source text) document-wide, or (display := summary | source | hidden) on an individual block.

There is no generated rendered fragment for external markup in this fork, and no --external-markup-render switch: the MD4Lean-backed fragment renderer that produced HTML-cache bodies for markup-only entries is among the deletions listed under Fork status. A consumer that needs rendered Markdown should author a native Verso body.

These ExternalMarkup attachments are primarily a porting aid for existing TeX or Markdown documents. Use slot names such as statement and proof when one Blueprint node corresponds to multiple informal markup witnesses.

Blueprint can separately record Level 1 original-source provenance for audit tools. Declare a source document with :::source_document and attach node-local source spans in a leading Verso metadata block:

:::source_document "paper"
%%%
title := "Representation Theory"
kind := .pdf
pdf := "source/paper.pdf"
%%%
:::

:::lemma_ "addition_right_identity"
%%%
source := {
  document := "paper"
  spans := #[
    {
      page := "12"
      pdf := some { path := "source/pages/page-12.pdf" }
    }
  ]
}
%%%

For every natural number $`n`, $`n + 0 = n`.
:::

Current behavior: source provenance is exported in the Blueprint manifest as sourceDocuments and per-entry sources, and kept hidden in rendered pages. Browser clients can resolve source-document ids with loadSourceDocument, load the complete catalog with loadSourceDocuments, or join entry source refs with declared documents using resolveSourceMetadata from api/data.mjs or api/preview.mjs. Manifest entries also carry source-location lookup results. Custom browser clients can call resolveLabel for Blueprint labels or resolveDeclaration for Lean declarations when they need jump-to-source targets. Rich audit-interface rendering is planned separately.

Rendering to HTML

Blueprint can render:

chapter pages
a dependency graph with blueprint_graph
an overview and progress summary page with blueprint_summary
a bibliography page with blueprint_bibliography
math-enabled previews and cross-links
associated Rust code panels for labeled inline Rust blocks

The graph page is interactive rather than static: it can expose a view switcher for grouped graphs, a legend popover, a Graph options control for direction and component-packing switches, and graph-node previews that can be configured as pinned or hover panels with docked or anchored placement.

Progress is computed automatically from the status of the associated Lean code and declarations, so the HTML summary and graph views stay aligned with the formal side. In particular, incomplete Lean declarations such as sorry contribute automatically to the reported progress state.

Metadata export

For common label, dependency, planning, and metadata queries, use lake exe vbp query. Lower-level tools can also dump the complete semantic manifest, its schema, and the rendered-fragment cache (blueprint-html-cache.json) used by preview consumers. The cache includes the hover payloads needed by cached Lean fragments. These are command-line flags passed to the generator entry point, such as --dump-manifest, --dump-html-cache, and --dump-schema. See doc/API.md for the current generated-data contract.

JavaScript API tooling

The browser APIs emitted under -verso-data/api/ remain plain JavaScript ESM. API documentation is written in JSDoc, rendered with Docdash, and TypeScript checks the public API entrypoints plus their direct support modules with allowJs and checkJs. The generated-site public browser entrypoints are api/preview.mjs, api/data.mjs, and api/graph.mjs; the other emitted JavaScript modules are private runtime support chunks for those entrypoints and generated pages. This first pass intentionally focuses on the custom-client API surface; broader private runtime coverage and noImplicitAny tightening are follow-up cleanup items. TypeScript users consume generated declaration files from dist/types; those files are build artifacts and are not tracked in source.

Useful maintainer commands:

npm run typecheck
npm run build:types
npm run check:types
npm run docs
npm run check:docs

The rendered API reference is deployed on GitHub Pages at leanprover.github.io/verso-blueprint/js-api/. CI also uploads the same generated HTML as the js-api-docs artifact on each ci.yml run for PR-local inspection.

Custom clients can import the generated preview module directly from a rendered site:

import { createPreview } from "./-verso-data/api/preview.mjs";

const preview = createPreview();
const container = document.querySelector("#target");
if (!container) throw new Error("Missing preview target");

await preview.renderNode(container, {
  label: "Chapter2:Problem2.11.6",
  externalMarkup: {
    prefer: [
      { language: "verso", slot: "statement" },
      {
        language: "markdown",
        slot: "original",
        render: async ({ raw }, target) => {
          target.replaceChildren(renderMarkdown(raw));
        }
      },
      { display: "source" }
    ]
  }
});

Widget

The widget surface is experimental. Import VersoBlueprint.Widget explicitly if you want to enable it.

Reference Blueprints

Reference blueprints are known Blueprint projects that this repository builds and publishes as release validation examples. They are useful for checking that the renderer still works on real projects and for inspecting representative generated output; they are not the starter template contract for new projects.

The current published catalog is selected from branch-policy.json and tests/harness/projects.json; those files are the source of truth for which reference projects publish on each Lean release line. Maintainers can inspect the current checkout's selected projects with python3 -m scripts.blueprint_reference_harness projects.

Each external Blueprint is published only for its intended current release. Noperthedron and Sphere Packing currently target v4.32.0; FLT and Carleson target v4.33.0. The in-repo starter template is a CI fixture rather than a public reference entry; it continues to validate every maintained release line.

Rendered Test Blueprints

The deployed test-fixture sites live under the GitHub Pages test-blueprints tree:

The distinction is:

the categorized test blueprint index is the directory page for all local HTML-producing test fixtures
preview_runtime_showcase is one specific standalone rendered site listed in that directory

Most entries in the test blueprint index are curated doc-backed fixtures. The showcase is different: it is a small standalone Blueprint package used for the browser/runtime regression path and for exercising richer cross-page behavior in one place.

Documentation

User Documentation

Read these in order:

project_template/README.md: copyable starter project and file layout
doc/GETTING_STARTED.md: first Blueprint walkthrough
doc/MANUAL.md: authoring and rendering reference
JavaScript API reference: browser-facing data, preview, graph, and shared type APIs
doc/API.md: documented Lean, generated-data, and browser APIs. Start with Choosing an API, then jump to Browser ESM APIs, Graph Data APIs, or Lean Graft and Render APIs.

Developer Documentation

doc/CONTRIBUTING.md: contribution conventions for this repository
doc/MAINTAINER_GUIDE.md: repository-local generation, validation, CI publication, and worktree workflow
scripts/README.md: lightweight guide to the repository scripts and harness entry points
doc/DESIGN_RATIONALE.md: architecture and design boundaries
doc/ROADMAP.md: active cleanup and follow-up work
doc/roadmap/README.md: scoped maintainer planning cards, upstream follow-up index, and card template

Agent Helper Skill

The repository includes an agent-facing skill under skills/verso-blueprint/ for Codex/Claude-style local coding agents. The skill teaches agents to use lake exe vbp ... for project discovery, build/serve previews, generated-data queries, and post-edit checks.

lake exe vbp build is the normal Blueprint generation interface for projects. It discovers the project generator entry point and runs it through Lake's Lean wrapper internally. Treat vbp query JSON as an unstable agent interface, not a public compatibility contract and not part of the documented integration API.

Maintainer CLI Split

The repository now uses two small maintainer CLIs instead of one large mixed surface:

python3 -m scripts.blueprint_harness Worktree creation, root release-branch checks, landing, and local coordination
python3 -m scripts.blueprint_reference_harness Reference-project generation, validation, cache sync, editable reference checkouts, and prune operations

The shell wrappers under scripts/ still front the common reference-generation and validation flows.

Acknowledgements

Verso Blueprint builds on:

Verso, the document system used to write and render Blueprint documents
Lean 4, the language and tooling used to elaborate the document and connect it to formal code

Verso Blueprint has been directly inspired by previous blueprint projects:

Patrick Massot's Lean blueprints
LeanArchitect
Side to side blueprints by Eric Vergo

We are very grateful to the authors of these projects for their hard work and contributions to the Lean community.

Name		Name	Last commit message	Last commit date
Latest commit History 884 Commits
.github		.github
doc		doc
project_template		project_template
scripts		scripts
skills/verso-blueprint		skills/verso-blueprint
src		src
static-web		static-web
tests		tests
.gitattributes		.gitattributes
.gitignore		.gitignore
AGENTS.md		AGENTS.md
LICENSE		LICENSE
NOTICE		NOTICE
README.md		README.md
branch-policy.json		branch-policy.json
jsdoc.json		jsdoc.json
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain
package-lock.json		package-lock.json
package.json		package.json
tsconfig.json		tsconfig.json
tsconfig.types.json		tsconfig.types.json

Navigation Menu

Repository files navigation

Showcase

Provenance & authorship

What this fork changes vs upstream

Wiring

Branch layout

Fork status: upstream capabilities not carried over

Start Here

Start a project

See real examples

Current Project Shape

Three-Level Blueprint Model

Core Features

Labeled nodes and rich directives

Connecting to Lean

Attached Rust code

Math, TeX, and external markup

Rendering to HTML

Metadata export

JavaScript API tooling

Widget

Reference Blueprints

Rendered Test Blueprints

Documentation

User Documentation

Developer Documentation

Agent Helper Skill

Maintainer CLI Split

Acknowledgements

About

Releases

Packages

Contributors

Languages

Folders and files

Latest commit

History

Repository files navigation

Showcase

Provenance & authorship

What this fork changes vs upstream

Wiring

Branch layout

Fork status: upstream capabilities not carried over

Start Here

Start a project

See real examples

Current Project Shape

Three-Level Blueprint Model

Core Features

Labeled nodes and rich directives

Connecting to Lean

Attached Rust code

Math, TeX, and external markup

Rendering to HTML

Metadata export

JavaScript API tooling

Widget

Reference Blueprints

Rendered Test Blueprints

Documentation

User Documentation

Developer Documentation

Agent Helper Skill

Maintainer CLI Split

Acknowledgements

About

Topics

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages