nx_wiedijk_100.nx

nx_wiedijk_100.nx -- Wiedijk Top 100 Mathematical Theorems corpus, registered against the v2 kernel via nx_lemma_import. Per user 2026-05-15: "wtf are we doing in preschool level when we can exceed". The Wiedijk Top 100 is a benchmark list (Freek Wiedijk, Nijmegen) of 100 theorems that proof assistants are scored against. As of 2024 the public scoreboard (Wiedijk's tracker): HOL Light: ~88 PROVED Isabelle: ~84 PROVED Coq: ~73 PROVED Mizar: ~73 PROVED ProofPower: ~46 Lean: growing fast (Mathlib4) Metamath: ~74 PVS: ~24 This corpus registers ALL 100 statements with honest per-entry provenance. Status meaning: PROVED_NATIVE <- we have a v2 NishiLang chain IMPORTED_TRUSTED <- known proved in named source system; we trust their verification (no native chain yet) IMPORTED_PENDING <- not yet in any imported corpus Honest framing: IMPORTED_TRUSTED is verification DEBT. We don't claim parity-by-quality with HOL Light just by importing -- the audit reports debt explicitly. This is the same framing Lean Mathport used to seed Mathlib4 from Mathlib3.