Reproducing the Formalizations, the Verifier, and the Builds

Last verified on macOS 15 (Apple Silicon, Darwin 24.6) with elan managing Lean toolchains (each repository pins its own via lean-toolchain), Python 3.12 with PreTeXt 2.43.2 for the paper builds, TeX Live (latexmk) for the PDF, and SageMath 10 (which provides GAP) for the finite-quotient verifier. Linux is expected to work identically for the Lean and verifier steps; only the site-build scripts assume BSD sed.

The pinned commit for this site release is shown in the footer. A clean build takes under an hour after the Mathlib cache download:

git clone https://github.com/roed-math/gq2-lean
cd gq2-lean
git checkout 0ffb3908c72f9a61bc1142567fb6bd9f2e67aaa3   # this release's pin
lake exe cache get     # downloads the pinned Mathlib build cache
lake build             # builds the GQ2 library; no sorry anywhere

The main theorem is GQ2.main_presentation_literal : Nonempty (ContinuousMulEquiv GammaA AbsGalQ2) in GQ2/PresentationLiteral.lean, and its equivalent finite-counting form is GQ2.SectionTen.main_surjection_count'. The axiom audit (every capstone theorem must print exactly the three standard Lean axioms plus the nine-interface literature census, with no sorry and no native_decide) is scripted:

scripts/check_axioms.sh

Expected output ends with every audited capstone reporting the standard three axioms (propext, Quot.sound, Classical.choice) plus the nine named GQ2.* interfaces, and nothing else. For a single declaration, #print axioms GQ2.main_presentation_literal inside the project gives the same list.

The standalone release deliberately has no root module, so build the capstone target directly:

git clone https://github.com/davidturturean/gq2-lean-turturean
cd gq2-lean-turturean
git checkout audit-11.1     # the audited standalone release
lake exe cache get
lake build Q2Presentation.PresentationCorrect

The release notes on that repository list its assumed inputs; the formalizations page explains the relation between the standalone and completed versions.

The comparator checks that an untrusted challenge statement is proved by the library with only the permitted axioms. In gq2-lean, the challenge/solution pair is Challenge.lean / Solution.lean with configuration in comparator-config.json (the permitted-axiom list is exactly the standard three plus the nine census interfaces):

lake build Solution

The challenge theorems (challenge_main_presentation_literal, challenge_main_presentation_literal_roe_unconditional) carry sorry in Challenge.lean by design (they are the untrusted statements) and are discharged by Solution.lean; audit them with #print axioms as above.

The verifier lives in the padicIGP repository and runs under Sage. It checks the presentation's predicted count of Galois extensions against the known count for each of the 5,402 test groups in verification/DATA/2/:

git clone https://github.com/roed314/padicIGP
cd padicIGP
git checkout a8fd2662ff8726059bee61aaf0720e23f9db3bba   # this release's pin
cd verification
# The committed DATA/2/rel.txt is the paper's presentation.  To test a
# different one, save it as verification/rel.txt (format: problem.tex);
# the paper's file is also reproduced in the manuscript's worked-examples
# appendix.
PYTHONHASHSEED=0 ./verify -j 8

Expected final line: Verification successful! with all 5,402 groups matching. The group inventory (DATA/2/gps.txt), the known counts it is checked against (DATA/2/cnts.txt), and the relator input (DATA/2/rel.txt) are mirrored with sha256 hashes on the verifier page and in status.json. Two practical notes: set PYTHONHASHSEED=0 so the resume cache stays valid across interrupted runs, and expect a multi-hour run at -j 8 on a laptop. Passing is strong evidence but checks only finitely many finite quotients; it is not a proof.

The paper and site are built with the public PaperForge pipeline applied to this project's source instance (the LaTeX draft, PreTeXt insertions, crosswalk data, and build scripts). Unlike the formalization and verifier repositories above, the source instance is not currently public; contact the first author for access. Every artifact the pipeline produces is published on this site: the interactive paper, the PDF, both blueprints, the API documentation subsets, and status.json. For the record, the build entry points from the instance root are:

scripts/build-web.sh        # LaTeX draft -> PreTeXt -> interactive HTML
scripts/build-arxiv.sh      # the arXiv-style PDF (stamps the manuscript date)
blueprint/scripts/ci-pages.sh       # Verso blueprint, Roe formalization
blueprint-gpt/scripts/ci-pages.sh   # Verso blueprint, Turturean formalization
scripts/build-leandocs.sh   # doc-gen4 API documentation subsets
scripts/build-site.sh       # assemble output/site/ (runs the status stamper)

Generated audit pages are re-derived from the live artifacts on every build: the axioms page from the docstring census of GQ2/Foundations/Axioms.lean (scripts/gen-axioms-page.py), the dependency graphs from the Lean environment's kernel-level dependency export, and the footer version identifiers on these pages from status.json (paperforge sitegen/gen_status.py, whose --check mode fails the build when any stamped page or count has drifted from the live artifacts).