Pat 定理全部证明过程 — R157-R171 (Complete Proof Process of the Pat Theorems)
Abstract
Aggregate package: the complete Pat theorem Lean corpus (81 Pat*.lean files from Formal/Toolkit) plus the claim ledger (R157-R171, 99 YAML). The exercise papers carrying the theorem statements have DOIs (16 records, see REFERENCES.md). lake build 3631 jobs, 0 sorry. CC BY-NC-ND 4.0.
Fields of Study & Subjects
Mathematics
Computing
and Information Processing
SAS software applications and methods
Logic
programming
and type systems
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 14 August 2026
- Document type
- Preprint