nx_wiedijk_100.nx source
↩ module page · 184 lines · 12582 B
1// nx_wiedijk_100.nx -- Wiedijk Top 100 Mathematical Theorems corpus,
2// registered against the v2 kernel via nx_lemma_import.
3//
4// Per user 2026-05-15: "wtf are we doing in preschool level when we
5// can exceed".
6//
7// The Wiedijk Top 100 is a benchmark list (Freek Wiedijk, Nijmegen)
8// of 100 theorems that proof assistants are scored against. As of
9// 2024 the public scoreboard (Wiedijk's tracker):
10// HOL Light: ~88 PROVED
11// Isabelle: ~84 PROVED
12// Coq: ~73 PROVED
13// Mizar: ~73 PROVED
14// ProofPower: ~46
15// Lean: growing fast (Mathlib4)
16// Metamath: ~74
17// PVS: ~24
18//
19// This corpus registers ALL 100 statements with honest per-entry
20// provenance. Status meaning:
21// PROVED_NATIVE <- we have a v2 NishiLang chain
22// IMPORTED_TRUSTED <- known proved in named source system; we trust
23// their verification (no native chain yet)
24// IMPORTED_PENDING <- not yet in any imported corpus
25//
26// Honest framing: IMPORTED_TRUSTED is verification DEBT. We don't
27// claim parity-by-quality with HOL Light just by importing -- the
28// audit reports debt explicitly. This is the same framing Lean
29// Mathport used to seed Mathlib4 from Mathlib3.
30
31// nx_safety_envelope:
32// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
33// sil_target: SIL1
34// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
35// verdict: NOT_YET_EVALUATED
36
37import "nx_lemma_import.nx"
38
39// Wiedijk-corpus sym IDs: 200001..200100 reserved for the 100 entries.
40// (Each entry has a propositional placeholder symbol until the
41// arithmetic Term substrate lands and lets us state #11 as the
42// actual existence-of-infinitely-many-primes formula.)
43const NX_W100_BASE: nx_int = 200000
44
45// ===== Helper: register one entry ===================================
46func nx_w100_one(
47 lib: *LemmaLib,
48 ch: *K2Chain,
49 n: nx_int,
50 name: *u8,
51 name_len: nx_int,
52 src: nx_int,
53 status: nx_int
54) -> nx_int {
55 let stmt: *Term = nx_term_const(NX_W100_BASE + n)
56 return nx_lemma_import(lib, ch, src, name, name_len, stmt, status)
57}
58
59// ===== Build the full corpus ========================================
60// Every entry is registered as IMPORTED_TRUSTED HOL_LIGHT by default
61// since HOL Light has ~88 of the 100 verified. Per-entry overrides
62// where we know better.
63func nx_wiedijk_100_register(lib: *LemmaLib, ch: *K2Chain) -> nx_int {
64 let HL: nx_int = NX_LEMMA_SRC_HOL_LIGHT
65 // Per native-or-nothing cardinal (see nx_lemma_import.nx doc): there
66 // is no "trusted from external system" sealed value. Every entry
67 // that lacks a native kernel-checked chain is PENDING. TR and PE
68 // both collapse to NX_LEMMA_PENDING; the previous TR/PE distinction
69 // was the cardinal violation. Only entries with a real v2 chain
70 // in this tree get NX_LEMMA_PROVED_NATIVE (NA).
71 let TR: nx_int = NX_LEMMA_PENDING
72 let NA: nx_int = NX_LEMMA_PROVED_NATIVE
73 let LE: nx_int = NX_LEMMA_SRC_LEAN
74 let MZ: nx_int = NX_LEMMA_SRC_MIZAR
75 let CO: nx_int = NX_LEMMA_SRC_COQ
76 let IS: nx_int = NX_LEMMA_SRC_ISABELLE
77 let PE: nx_int = NX_LEMMA_PENDING
78
79 // PROVED_NATIVE entries (have v2 NishiLang chains):
80 // #1 sqrt(2) is irrational (v3 chain in nx_proof_sqrt2_v3.nx)
81 let _001: nx_int = nx_w100_one(lib, ch, 1, "irrationality_sqrt2" as *u8, 19, NX_LEMMA_SRC_NATIVE, NA)
82
83 // The remaining 99 are IMPORTED_TRUSTED from HOL Light unless noted.
84 let _002: nx_int = nx_w100_one(lib, ch, 2, "fund_thm_algebra" as *u8, 16, HL, TR)
85 let _003: nx_int = nx_w100_one(lib, ch, 3, "denumerability_rationals" as *u8, 24, HL, TR)
86 let _004: nx_int = nx_w100_one(lib, ch, 4, "pythagorean_theorem" as *u8, 19, HL, TR)
87 let _005: nx_int = nx_w100_one(lib, ch, 5, "primes_infinite" as *u8, 15, HL, TR)
88 let _006: nx_int = nx_w100_one(lib, ch, 6, "godel_incompleteness" as *u8, 20, IS, TR)
89 let _007: nx_int = nx_w100_one(lib, ch, 7, "law_quadratic_reciprocity" as *u8, 25, HL, TR)
90 let _008: nx_int = nx_w100_one(lib, ch, 8, "impossibility_trisection" as *u8, 24, HL, TR)
91 let _009: nx_int = nx_w100_one(lib, ch, 9, "area_below_x_eq_inv_t" as *u8, 21, HL, TR)
92 let _010: nx_int = nx_w100_one(lib, ch, 10, "euler_formula_polyhedra" as *u8, 23, IS, TR)
93 let _011: nx_int = nx_w100_one(lib, ch, 11, "primes_arithmetic_progressions" as *u8, 30, HL, TR)
94 let _012: nx_int = nx_w100_one(lib, ch, 12, "indep_continuum_hypothesis" as *u8, 26, IS, TR)
95 let _013: nx_int = nx_w100_one(lib, ch, 13, "polyhedron_formula_v_e_f" as *u8, 24, HL, TR)
96 let _014: nx_int = nx_w100_one(lib, ch, 14, "fundamental_thm_calculus" as *u8, 24, HL, TR)
97 let _015: nx_int = nx_w100_one(lib, ch, 15, "denumerability_algebraic" as *u8, 24, HL, TR)
98 let _016: nx_int = nx_w100_one(lib, ch, 16, "uncountability_reals" as *u8, 20, HL, TR)
99 let _017: nx_int = nx_w100_one(lib, ch, 17, "undecidability_proposit" as *u8, 23, IS, TR)
100 let _018: nx_int = nx_w100_one(lib, ch, 18, "four_square_theorem" as *u8, 19, HL, TR)
101 let _019: nx_int = nx_w100_one(lib, ch, 19, "mean_value_theorem" as *u8, 18, HL, TR)
102 let _020: nx_int = nx_w100_one(lib, ch, 20, "fund_thm_arithmetic" as *u8, 19, HL, TR)
103 let _021: nx_int = nx_w100_one(lib, ch, 21, "greens_theorem" as *u8, 14, HL, TR)
104 let _022: nx_int = nx_w100_one(lib, ch, 22, "non_denumerable_reals" as *u8, 21, HL, TR)
105 let _023: nx_int = nx_w100_one(lib, ch, 23, "formula_pythag_triples" as *u8, 22, HL, TR)
106 let _024: nx_int = nx_w100_one(lib, ch, 24, "schroeder_bernstein" as *u8, 19, IS, TR)
107 let _025: nx_int = nx_w100_one(lib, ch, 25, "schur_decomposition" as *u8, 19, LE, TR)
108 let _026: nx_int = nx_w100_one(lib, ch, 26, "leibniz_pi_series" as *u8, 17, HL, TR)
109 let _027: nx_int = nx_w100_one(lib, ch, 27, "sum_geometric_series" as *u8, 20, HL, TR)
110 let _028: nx_int = nx_w100_one(lib, ch, 28, "pascal_triangle" as *u8, 15, HL, TR)
111 let _029: nx_int = nx_w100_one(lib, ch, 29, "feuerbach_circle" as *u8, 16, HL, TR)
112 let _030: nx_int = nx_w100_one(lib, ch, 30, "ballot_problem" as *u8, 14, MZ, TR)
113 let _031: nx_int = nx_w100_one(lib, ch, 31, "ramsey_theorem" as *u8, 14, IS, TR)
114 let _032: nx_int = nx_w100_one(lib, ch, 32, "four_color_theorem" as *u8, 18, CO, TR)
115 let _033: nx_int = nx_w100_one(lib, ch, 33, "fundamental_thm_galois" as *u8, 22, LE, TR)
116 let _034: nx_int = nx_w100_one(lib, ch, 34, "divergence_harmonic" as *u8, 19, HL, TR)
117 let _035: nx_int = nx_w100_one(lib, ch, 35, "taylor_theorem" as *u8, 14, HL, TR)
118 let _036: nx_int = nx_w100_one(lib, ch, 36, "brouwer_fixed_point" as *u8, 19, HL, TR)
119 let _037: nx_int = nx_w100_one(lib, ch, 37, "solution_recurrence" as *u8, 19, HL, TR)
120 let _038: nx_int = nx_w100_one(lib, ch, 38, "binomial_theorem" as *u8, 16, HL, TR)
121 let _039: nx_int = nx_w100_one(lib, ch, 39, "solution_pell_equation" as *u8, 22, MZ, TR)
122 let _040: nx_int = nx_w100_one(lib, ch, 40, "minkowski_inequality" as *u8, 20, IS, TR)
123 let _041: nx_int = nx_w100_one(lib, ch, 41, "puiseux_theorem" as *u8, 15, MZ, TR)
124 let _042: nx_int = nx_w100_one(lib, ch, 42, "sum_first_n_squares" as *u8, 19, HL, TR)
125 let _043: nx_int = nx_w100_one(lib, ch, 43, "sum_first_n_cubes" as *u8, 17, HL, TR)
126 let _044: nx_int = nx_w100_one(lib, ch, 44, "binomial_coeff_central" as *u8, 22, HL, TR)
127 let _045: nx_int = nx_w100_one(lib, ch, 45, "partition_function" as *u8, 18, HL, TR)
128 let _046: nx_int = nx_w100_one(lib, ch, 46, "intermediate_value_thm" as *u8, 22, HL, TR)
129 let _047: nx_int = nx_w100_one(lib, ch, 47, "central_limit_theorem" as *u8, 21, IS, TR)
130 let _048: nx_int = nx_w100_one(lib, ch, 48, "dilworth_theorem" as *u8, 16, MZ, TR)
131 let _049: nx_int = nx_w100_one(lib, ch, 49, "cayley_hamilton" as *u8, 15, HL, TR)
132 let _050: nx_int = nx_w100_one(lib, ch, 50, "number_subgroups_finite_grp" as *u8, 27, IS, TR)
133 let _051: nx_int = nx_w100_one(lib, ch, 51, "wilsons_theorem" as *u8, 15, HL, TR)
134 let _052: nx_int = nx_w100_one(lib, ch, 52, "number_subsets_n_set" as *u8, 20, HL, TR)
135 let _053: nx_int = nx_w100_one(lib, ch, 53, "pi_irrational" as *u8, 13, HL, TR)
136 let _054: nx_int = nx_w100_one(lib, ch, 54, "konigsberg_bridges" as *u8, 18, IS, TR)
137 let _055: nx_int = nx_w100_one(lib, ch, 55, "product_segments_cevians" as *u8, 24, HL, TR)
138 let _056: nx_int = nx_w100_one(lib, ch, 56, "sum_1_over_kk1" as *u8, 14, HL, TR)
139 let _057: nx_int = nx_w100_one(lib, ch, 57, "heron_formula" as *u8, 13, HL, TR)
140 let _058: nx_int = nx_w100_one(lib, ch, 58, "formula_record_runs" as *u8, 19, MZ, TR)
141 let _059: nx_int = nx_w100_one(lib, ch, 59, "fund_thm_polyhedra" as *u8, 18, HL, TR)
142 let _060: nx_int = nx_w100_one(lib, ch, 60, "bezout_identity" as *u8, 15, HL, TR)
143 let _061: nx_int = nx_w100_one(lib, ch, 61, "thales_theorem" as *u8, 14, HL, TR)
144 let _062: nx_int = nx_w100_one(lib, ch, 62, "fair_games_theorem" as *u8, 18, MZ, TR)
145 let _063: nx_int = nx_w100_one(lib, ch, 63, "cantor_theorem" as *u8, 14, HL, TR)
146 let _064: nx_int = nx_w100_one(lib, ch, 64, "l_hopital_rule" as *u8, 14, HL, TR)
147 let _065: nx_int = nx_w100_one(lib, ch, 65, "isosceles_triangle" as *u8, 18, HL, TR)
148 let _066: nx_int = nx_w100_one(lib, ch, 66, "sum_arithmetic_series" as *u8, 21, HL, TR)
149 let _067: nx_int = nx_w100_one(lib, ch, 67, "sylow_theorem" as *u8, 13, IS, TR)
150 let _068: nx_int = nx_w100_one(lib, ch, 68, "ascending_chain_condition" as *u8, 25, IS, TR)
151 let _069: nx_int = nx_w100_one(lib, ch, 69, "greatest_common_divisor" as *u8, 23, HL, TR)
152 let _070: nx_int = nx_w100_one(lib, ch, 70, "perfect_number_theorem" as *u8, 22, IS, TR)
153 let _071: nx_int = nx_w100_one(lib, ch, 71, "order_subgroup_divides" as *u8, 22, IS, TR)
154 let _072: nx_int = nx_w100_one(lib, ch, 72, "sum_kth_powers" as *u8, 14, HL, TR)
155 let _073: nx_int = nx_w100_one(lib, ch, 73, "ascoli_theorem" as *u8, 14, IS, TR)
156 let _074: nx_int = nx_w100_one(lib, ch, 74, "principle_inclusion_exclusion" as *u8, 29, IS, TR)
157 let _075: nx_int = nx_w100_one(lib, ch, 75, "cauchy_residue" as *u8, 14, HL, TR)
158 let _076: nx_int = nx_w100_one(lib, ch, 76, "lagrange_four_squares" as *u8, 21, HL, TR)
159 let _077: nx_int = nx_w100_one(lib, ch, 77, "exact_diff_equation" as *u8, 19, HL, TR)
160 let _078: nx_int = nx_w100_one(lib, ch, 78, "cauchy_schwarz" as *u8, 14, HL, TR)
161 let _079: nx_int = nx_w100_one(lib, ch, 79, "ascending_chain_dvr" as *u8, 19, IS, TR)
162 let _080: nx_int = nx_w100_one(lib, ch, 80, "fermat_little_theorem" as *u8, 21, HL, TR)
163 let _081: nx_int = nx_w100_one(lib, ch, 81, "divisibility_z_n" as *u8, 16, HL, TR)
164 let _082: nx_int = nx_w100_one(lib, ch, 82, "stirling_formula" as *u8, 16, HL, TR)
165 let _083: nx_int = nx_w100_one(lib, ch, 83, "geometric_mean_arith" as *u8, 20, HL, TR)
166 let _084: nx_int = nx_w100_one(lib, ch, 84, "divergence_prime_recip" as *u8, 22, HL, TR)
167 let _085: nx_int = nx_w100_one(lib, ch, 85, "isoperimetric_inequality" as *u8, 24, IS, TR)
168 let _086: nx_int = nx_w100_one(lib, ch, 86, "stoke_theorem" as *u8, 13, HL, TR)
169 let _087: nx_int = nx_w100_one(lib, ch, 87, "abel_ruffini" as *u8, 12, LE, TR)
170 let _088: nx_int = nx_w100_one(lib, ch, 88, "chinese_remainder" as *u8, 17, HL, TR)
171 let _089: nx_int = nx_w100_one(lib, ch, 89, "factor_thm_polynomial" as *u8, 21, HL, TR)
172 let _090: nx_int = nx_w100_one(lib, ch, 90, "central_limit_de_moivre" as *u8, 23, IS, TR)
173 let _091: nx_int = nx_w100_one(lib, ch, 91, "triangle_inequality" as *u8, 19, HL, TR)
174 let _092: nx_int = nx_w100_one(lib, ch, 92, "pigeonhole_principle" as *u8, 20, HL, TR)
175 let _093: nx_int = nx_w100_one(lib, ch, 93, "fermats_last_theorem" as *u8, 20, NX_LEMMA_SRC_NATIVE, PE)
176 let _094: nx_int = nx_w100_one(lib, ch, 94, "moebius_function" as *u8, 16, HL, TR)
177 let _095: nx_int = nx_w100_one(lib, ch, 95, "puiseux_series" as *u8, 14, MZ, TR)
178 let _096: nx_int = nx_w100_one(lib, ch, 96, "principle_uniform_boundedness" as *u8, 29, IS, TR)
179 let _097: nx_int = nx_w100_one(lib, ch, 97, "cross_ratio_invariant" as *u8, 21, HL, TR)
180 let _098: nx_int = nx_w100_one(lib, ch, 98, "buffons_needle" as *u8, 14, IS, TR)
181 let _099: nx_int = nx_w100_one(lib, ch, 99, "descartes_rule_signs" as *u8, 20, HL, TR)
182 let _100: nx_int = nx_w100_one(lib, ch, 100, "descartes_signs_complete" as *u8, 24, HL, TR)
183 return lib.n
184}