These papers describe repository revisions from August and September 2026. Their APIs, binaries, theorem statements, and reproduction commands belong to those revisions. Each report preserves its source, PDF, and evidence. The current system has separate manuals for the LeanExe compiler and the verified compiler, with the current numerical results in the numerical index.
| Work | Subject | Record |
|---|---|---|
| Exact-artifact verification paper | Complete system, evaluation, trusted base, and roadmap. | Root LaTeX source and review record. |
| Structured LTG note | Selective retrieval from the growing proof knowledge base. | marXiv:2608.00029 |
| Frame-accessor note | Compiler-generated frame projections and their proof screens. | marXiv:2608.00034 |
| Tactic-retrieval note | Goal-shape tactic indexing, selection, and accepted proof evidence. | marXiv:2608.00036 |
| The LeanExe Subset | Runtime typing, extraction, packed storage, and per-compilation proof obligations. | marXiv:2609.00005 |
| Reconstructed Euler report | Exact-binary solver proof, physical numerical guarantees, and 192-grid and 800-grid results. | marXiv:2609.00006 |
| Cached GPT-2 verification report | Exact execution of the Lean GPT-2/128 recurrence, packed FP32 arithmetic, allocation sufficiency, and command-line inference. | marXiv:2609.00011 |
| WGSL verification report | Checked shader compilation, packed matrix equalities, and conditional hybrid GPT-2/128 execution. | marXiv:2609.00012 |
| Comprehensive GPT-2 report | LeanExe, CPU artifact and WGSL proofs, theorem structure, literature comparison, and browser execution images. | marXiv:2609.00014 |
| Quantized GPT-2 report | Grouped INT8 arithmetic, exact binary and cached-session proofs, accuracy diagnosis, runtime measurements, and numerical bounds. | marXiv:2609.00018 |
| Drone verification report | Finite-graph optimality, continuous flight safety, generated-model execution, and five terrain runs. | marXiv:2609.00019 |
The root manuscript consists of four publication files:
- Manuscript source: the complete LaTeX document.
- Bibliography: thirty-two cited primary papers, specifications, and software records.
- Rendered paper: the generated eighteen-page PDF.
- Review record: the technical, editorial, and acceptance review passes applied before the final build.
Build the document by running the commands below from this directory. The first LaTeX pass creates the citation inventory, BibTeX generates the bibliography, and the final two LaTeX passes resolve citations, references, and PDF outlines. A clean build has no undefined citation, undefined reference, overfull-box, or BibTeX warnings.
pdflatex -interaction=nonstopmode -halt-on-error main.tex
bibtex main
pdflatex -interaction=nonstopmode -halt-on-error main.tex
pdflatex -interaction=nonstopmode -halt-on-error main.texThe anonymous author field and generic article class are placeholders. An arXiv submission needs the author list, affiliations, subject classification, license selection, and the final immutable LeanExe release identifier. The final release record also needs a matching cold-checkout receipt for the revision that contains every reported result.