Mathematics to a typed proof obligation

Live Formalization

Render a sampling-theory statement, inspect a reviewed or deterministic Lean candidate, run the pinned compiler locally, and export unresolved work into the ASTIS hierarchy.

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
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`
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.