PNBA Identity Physics ProofPress: Lean 4/Markdown to LaTeX Conversion Tool for Formally Verified Research uuia.app/proofpress

Abstract ProofPress is a standalone, browser-based conversion tool that transforms Lean 4 formal proof files into Overleaf-ready LaTeX documents. It operates in two modes: an LDP mode tuned to the SNSFT corpus conventions, and a General mode compatible with any standard Lean 4 file. The tool extracts theorem names, human-readable descriptions, return types, and LDP step annotations directly from the source file, populates a structured academic paper template, and produces a .tex file ready for journal submission. ProofPress requires no installation, no server, and no external dependencies. It is distributed as a single HTML file that executes entirely in the browser. The tool addresses a real and underserved gap in the formal verification ecosystem: the absence of a direct, low-friction pathway from machine-verified proof to publication-ready academic document. By eliminating the manual transcription step that currently stands between a formally verified corpus and its presentation to the scientific community, ProofPress lowers the barrier to publication for researchers working in Lean 4. 1. Motivation Formal verification produces machine-checked proofs with guarantees no informal mathematical argument can provide. The Lean 4 theorem prover, in conjunction with the Mathlib library, has become the standard environment for formally verified mathematics across an increasingly broad range of domains — from number theory and algebra to physics, materials science, and cognitive science. The research community has taken notice: high-profile formalizations such as Terry Tao's Polynomial Freiman-Ruzsa proof (2023) have demonstrated that formal verification can operate at the frontier of mathematical research rather than merely audit classical results. Despite this momentum, a fundamental asymmetry persists. Formally verified work exists simultaneously in two disconnected registers: the .lean file that the compiler accepts, and the academic paper that peer reviewers read. These are not interchangeable artifacts. The .lean file contains tactic proofs, namespace structures, and machine-readable syntax that journals do not accept. The academic paper requires prose exposition, LaTeX formatting, and structured narrative that the Lean compiler ignores. Translating between them is currently a manual process: a researcher must retype or copy-paste theorem statements, strip tactic proofs, escape special characters, apply LaTeX formatting, and restructure the entire document for journal conventions. For small corpora this is inconvenient. For large corpora it is a genuine bottleneck. The SNSFT corpus, for example, contains 200,000+ theorems across 3,000,000+ lines of Lean 4 and Coq/Rocq — a body of formally verified work spanning physics, chemistry, psychology, mathematics, and identity theory. Manually transcribing even a subset of this corpus into publication-ready format represents a significant and unnecessary cost. ProofPress addresses this bottleneck directly. It does not replace the intellectual work of writing a paper — the prose, the framing, the argument — but it eliminates the mechanical transcription step that precedes it, allowing researchers to spend their time on what matters. 2. Related Work Patrick Massot's Lean Blueprint (used by Terry Tao in the Polynomial Freiman-Ruzsa formalization, 2023) generates LaTeX/Lean hybrid documents from Lean source, designed for blueprint-style proof navigation. Blueprint targets collaborative proof development and proof readability within the Lean community. ProofPress targets a different output and a different audience: standard academic paper format suitable for external journal submission, not internal proof navigation. The two tools are complementary rather than competing.