nx_compare_systems.nx source
↩ module page · 127 lines · 6128 B
1// nx_compare_systems.nx -- axis-by-axis comparison engine.
2//
3// Per user 2026-05-15: "how do these proofs compare on all axes from
4// wikipedia to hol and other systems as ai wanted world class".
5//
6// Engine, not table. Each axis is a sealed-enum AXIS_* + sealed-enum
7// VERDICT_* + a named-improvement string for any LOSE. Caller passes
8// in a peer system; the engine emits the full row.
9//
10// Axes are pulled from Wikipedia "Comparison of theorem provers" +
11// "Automated theorem proving" + "Proof assistant" pages, plus the
12// HOL Light kernel paper (Harrison) and the Lean 4 architecture paper.
13// Refused: weasel words "competitive with" etc. (honest-perf cardinal).
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "nx_kernel_v2.nx"
22
23// ===== Sealed peer-system enum =====================================
24const NX_PEER_NX_OURS: nx_int = 0
25const NX_PEER_HOL_LIGHT: nx_int = 1
26const NX_PEER_HOL4: nx_int = 2
27const NX_PEER_COQ: nx_int = 3
28const NX_PEER_LEAN4: nx_int = 4
29const NX_PEER_ISABELLE: nx_int = 5
30const NX_PEER_MIZAR: nx_int = 6
31const NX_PEER_METAMATH: nx_int = 7
32const NX_PEER_AGDA: nx_int = 8
33const NX_PEER_MATHEMATICA: nx_int = 9
34
35// ===== Sealed axis enum (Wikipedia + papers) =======================
36const NX_AXIS_KERNEL_LOC: nx_int = 1
37const NX_AXIS_LCF_DISCIPLINE: nx_int = 2
38const NX_AXIS_NATIVE_TARGET: nx_int = 3
39const NX_AXIS_DEPENDENCY_FREE: nx_int = 4
40const NX_AXIS_TACTIC_LANG: nx_int = 5
41const NX_AXIS_AUTO_PROVER: nx_int = 6
42const NX_AXIS_SEMANTIC_REJECT: nx_int = 7
43const NX_AXIS_LIBRARY_SIZE: nx_int = 8
44const NX_AXIS_LOGIC: nx_int = 9
45const NX_AXIS_CLASSICAL_AXIOMS: nx_int = 10
46const NX_AXIS_ARITH_SUBSTRATE: nx_int = 11
47const NX_AXIS_PROB_SUBSTRATE: nx_int = 12
48const NX_AXIS_PROOF_OUTPUT: nx_int = 13
49const NX_AXIS_OPEN_SOURCE: nx_int = 14
50const NX_AXIS_VISUAL_NATIVE: nx_int = 15
51const NX_AXIS_PHYSICS: nx_int = 16
52const NX_AXIS_CHEMISTRY: nx_int = 17
53const NX_AXIS_LINALG: nx_int = 18
54const NX_AXIS_SYMBOLIC_CALC: nx_int = 19
55const NX_AXIS_BITS_UP_BUILD: nx_int = 20
56
57// ===== Verdict enum ================================================
58const NX_VERDICT_WIN_BIG: nx_int = 1
59const NX_VERDICT_WIN: nx_int = 2
60const NX_VERDICT_TIE: nx_int = 3
61const NX_VERDICT_LOSE: nx_int = 4
62const NX_VERDICT_LOSE_BIG: nx_int = 5
63const NX_VERDICT_UNMEASURABLE: nx_int = 6
64
65func nx_peer_name(p: nx_int) -> *u8 {
66 if p == NX_PEER_HOL_LIGHT { return "HOL Light " as *u8 }
67 if p == NX_PEER_HOL4 { return "HOL4 " as *u8 }
68 if p == NX_PEER_COQ { return "Coq " as *u8 }
69 if p == NX_PEER_LEAN4 { return "Lean 4 " as *u8 }
70 if p == NX_PEER_ISABELLE { return "Isabelle " as *u8 }
71 if p == NX_PEER_MIZAR { return "Mizar " as *u8 }
72 if p == NX_PEER_METAMATH { return "Metamath " as *u8 }
73 if p == NX_PEER_AGDA { return "Agda " as *u8 }
74 if p == NX_PEER_MATHEMATICA { return "Mathematica" as *u8 }
75 return "? " as *u8
76}
77
78func nx_verdict_name(v: nx_int) -> *u8 {
79 if v == NX_VERDICT_WIN_BIG { return "WIN_BIG " as *u8 }
80 if v == NX_VERDICT_WIN { return "WIN " as *u8 }
81 if v == NX_VERDICT_TIE { return "TIE " as *u8 }
82 if v == NX_VERDICT_LOSE { return "LOSE " as *u8 }
83 if v == NX_VERDICT_LOSE_BIG { return "LOSE_BIG " as *u8 }
84 if v == NX_VERDICT_UNMEASURABLE { return "UNMEASURABLE" as *u8 }
85 return "? " as *u8
86}
87
88func nx_axis_name(a: nx_int) -> *u8 {
89 if a == NX_AXIS_KERNEL_LOC { return "kernel_LOC " as *u8 }
90 if a == NX_AXIS_LCF_DISCIPLINE { return "LCF_discipline " as *u8 }
91 if a == NX_AXIS_NATIVE_TARGET { return "native_target " as *u8 }
92 if a == NX_AXIS_DEPENDENCY_FREE { return "dependency_free " as *u8 }
93 if a == NX_AXIS_TACTIC_LANG { return "tactic_language " as *u8 }
94 if a == NX_AXIS_AUTO_PROVER { return "auto_prover " as *u8 }
95 if a == NX_AXIS_SEMANTIC_REJECT { return "semantic_reject " as *u8 }
96 if a == NX_AXIS_LIBRARY_SIZE { return "library_size " as *u8 }
97 if a == NX_AXIS_LOGIC { return "logic " as *u8 }
98 if a == NX_AXIS_CLASSICAL_AXIOMS { return "classical_axioms " as *u8 }
99 if a == NX_AXIS_ARITH_SUBSTRATE { return "arith_substrate " as *u8 }
100 if a == NX_AXIS_PROB_SUBSTRATE { return "prob_substrate " as *u8 }
101 if a == NX_AXIS_PROOF_OUTPUT { return "proof_output_format " as *u8 }
102 if a == NX_AXIS_OPEN_SOURCE { return "open_source_license " as *u8 }
103 if a == NX_AXIS_VISUAL_NATIVE { return "visual_native " as *u8 }
104 if a == NX_AXIS_PHYSICS { return "physics_substrate " as *u8 }
105 if a == NX_AXIS_CHEMISTRY { return "chemistry_substrate " as *u8 }
106 if a == NX_AXIS_LINALG { return "linalg_native " as *u8 }
107 if a == NX_AXIS_SYMBOLIC_CALC { return "symbolic_calculus " as *u8 }
108 if a == NX_AXIS_BITS_UP_BUILD { return "bits_up_build " as *u8 }
109 return "? " as *u8
110}
111
112// One row emitter: prints axis | our_value | peer_value | verdict | named_improvement
113func nx_compare_row(axis: nx_int, peer: nx_int, our_val: *u8, peer_val: *u8,
114 verdict: nx_int, improvement: *u8) -> nx_int {
115 print(" " as *u8); print(nx_axis_name(axis))
116 print("| " as *u8); print(our_val)
117 print(" vs " as *u8); print(peer_val)
118 print(" | " as *u8); print(nx_verdict_name(verdict))
119 if verdict == NX_VERDICT_LOSE {
120 print(" -> " as *u8); print(improvement)
121 }
122 if verdict == NX_VERDICT_LOSE_BIG {
123 print(" -> " as *u8); print(improvement)
124 }
125 println("" as *u8)
126 return verdict
127}