Mathematics to a typed proof obligation

Live Formalization

Follow one source theorem step by step, keep recursive calls and error budgets visible, ask a source-grounded assistant, and hand an exact candidate to Lean without confusing explanation, compilation, and reviewed proof.

Research proof tracker

Read, question, export, verify

The selected source theorem, proof step, assumptions, ledger entries and compiled support are loaded from the same metadata that builds the companion reader. The assistant may explain or propose code; only the separate Lean and source-review gates can certify it.

Source contextPinned

AI responseNot requested

Lean certificateSeparate gate

Source reviewNot implied

Selected mathematical step

Loading…

Open

Source anchor
Truth boundary

Assumptions in scope

Lean support attached to this step

Recursive bookkeeping

Call and error ledger

Tracked quantities

Symbol	Meaning	Update	Role

Error flow

Human–AI–Lean handoff

Ask about this exact proof step

Checking API mode

Optional question

Choose an action. In static mode the site creates a bounded prompt that can be copied into ChatGPT or Codex; local API mode can answer here.

Every response is labelled AI explanation — unverified. It cannot turn a node blue, modify the Registry, or replace independent source review.

Lean candidate lab

Inspect and compile an exact snippet

Use this lower-level panel after the research tracker has fixed the mathematical statement and remaining obligation.

TranslationUnresolved

LeanNot compiled

ProofUnproved

ReviewNot reviewed

Source mathematics

Statement and context

LaTeX statement

Plain-language interpretation

Source anchor Preferred module

Formal candidate

Lean source

A successful compile checks this exact snippet. It does not establish source equivalence or prove an unfilled theorem.

Lean diagnostics

Load a reviewed mapping or enter a new statement.

Retrieval and obligations

Samplinglib

Mathlib

Assumptions

Open obligations

Semantic notes

Execution boundary

Static reading and local verification are different products

Capability	Static Pages	Local verified mode
Render LaTeX and load 77 reviewed mappings	Available	Available
Browse declaration dependencies and exact source anchors	Available	Available
Track a source theorem step-by-step with recursive-call and error ledgers	Available	Available
Download a paper-scoped research pack or visual ChatGPT/MCP App	Available	Available
Ask a source-bounded AI assistant	Prompt export	Optional Responses API; output remains unverified
Export ASTIS typed-artifact packets	Available	Available
Generate a deterministic candidate for supported templates	Unavailable	Available through `/api/formalize`
Execute the pinned Lean compiler	Unavailable	Available through `/api/compile` only when the active version exactly matches `lean-toolchain`
General semantic translation or autonomous proof acceptance	Not claimed	Not claimed

Local execution policy

The compiler service binds only to loopback, serializes compilation, limits request size and time, writes snippets only to a system temporary directory, and never modifies repository source. It is a developer tool, not a hardened public code-execution sandbox. Keep it behind the documented private preview path.

Packet handoff

flowchart LR
  S["Chewi source anchor<br/>chapter · section · page · equation"] --> E["ASTIS faithful exposition"]
  E --> R["Rigorous detail packet"]
  R --> D["Lean declaration"]
  D --> F["Lean source file"]
  D --> T["Tests / build gate"]
  D --> G["Registry entry"]
  G --> P["Generated site status"]
  T --> P

Exports preserve the analytic_contract, formalization_map, proof_attempt, and review boundaries consumed by ASTIS.