Paste or drop a Lean 4 corpus file. ProofPress parses the header, extracts theorems, and outputs an Overleaf-ready .tex — formatted to Identity Physics paper standard. One job. Done right.
PP · Because formally verified work deserves formally typeset output.
How It Works — Four Modes
LDP Paste a single Lean 4 file. ProofPress parses SNSFT corpus conventions — coordinate, DOI, ORCID, anchor constant — and outputs a locked-front-matter Identity Physics paper draft.
MD Markdown-first mode for general paper drafts that aren't tied to corpus front-matter conventions.
CHAIN Paste a master file's own import lines. ProofPress resolves each one — local files first (drop them in, matched by filename), GitHub pull only as fallback — and assembles one LaTeX paper, one subsection per resolved module, in import order.
COMBINE Same resolution as CHAIN, but the output is a single raw .lean file instead of a paper: imports deduped, per-file import lines stripped, bodies concatenated with provenance comments naming each source.
No GitHub write access required. Drop files in directly, or connect a read-only pull — pushing to a repository is a separate, explicit step, never a side effect of converting or combining.
Export formats:.tex · .lean · .pdf · .rtf — the PDF and RTF paths both handle the corpus's heavy use of Unicode math symbols correctly. PDF output is rendered as page images, not selectable text — use it for Overleaf/arXiv submission or Zenodo deposit. The Word-compatible .rtf export stays fully selectable, searchable text, which is why it’s the format that feeds directly into KDP and other print-on-demand publishing pipelines.
LDP mode — parses Identity Physics corpus conventions. Populates coordinate, DOI, ORCID, anchor constant, locked front matter. Output is an Identity Physics paper.
LEAN INPUT
paste .lean file content or drop file below
⬆ DROP .LEAN FILE OR CLICK TO BROWSE
⬆ DROP THE IMPORTED .LEAN FILES HERE (optional) — matched by name before falling back to GitHub
awaiting input
LATEX OUTPUT
overleaf-ready · copy or download
OPTIONS:
OPTIONS:
no output yet
GITHUB PUSH / PULL · v1.2
push .tex to your repo · or pull an import chain in CHAIN mode
GITHUB PAT
REPO
TARGET PATH (push)
IMPORT ROOT (chain)
pushes .tex + session JSON · PAT stored in memory only · never persisted