Paste or drop a Lean 4 corpus file. ProofPress parses the header, extracts theorems, and outputs an Overleaf-ready .tex — formatted to SNSFT paper standard. One job. Done right.
PP · Because formally verified work deserves formally typeset output.
LDP mode — parses SNSFT 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