nx_compare_systems.nx
buildroot/runtime/nx_compare_systems.nx
about
nx_compare_systems.nx -- axis-by-axis comparison engine.
Per user 2026-05-15: "how do these proofs compare on all axes from
wikipedia to hol and other systems as ai wanted world class".
Engine, not table. Each axis is a sealed-enum AXIS_* + sealed-enum
VERDICT_* + a named-improvement string for any LOSE. Caller passes
in a peer system; the engine emits the full row.
Axes are pulled from Wikipedia "Comparison of theorem provers" +
"Automated theorem proving" + "Proof assistant" pages, plus the
HOL Light kernel paper (Harrison) and the Lean 4 architecture paper.
Refused: weasel words "competitive with" etc. (honest-perf cardinal).
dependencies 1 imports · 1 importers
imports: nx_kernel_v2.nx
imported by: nx_compare_systems_test.nx
structs
| none |
consts
| 24 | const NX_PEER_NX_OURS: nx_int = 0 |
| 25 | const NX_PEER_HOL_LIGHT: nx_int = 1 |
| 26 | const NX_PEER_HOL4: nx_int = 2 |
| 27 | const NX_PEER_COQ: nx_int = 3 |
| 28 | const NX_PEER_LEAN4: nx_int = 4 |
| 29 | const NX_PEER_ISABELLE: nx_int = 5 |
| 30 | const NX_PEER_MIZAR: nx_int = 6 |
| 31 | const NX_PEER_METAMATH: nx_int = 7 |
| 32 | const NX_PEER_AGDA: nx_int = 8 |
| 33 | const NX_PEER_MATHEMATICA: nx_int = 9 |
| 36 | const NX_AXIS_KERNEL_LOC: nx_int = 1 |
| 37 | const NX_AXIS_LCF_DISCIPLINE: nx_int = 2 |
| 38 | const NX_AXIS_NATIVE_TARGET: nx_int = 3 |
| 39 | const NX_AXIS_DEPENDENCY_FREE: nx_int = 4 |
| 40 | const NX_AXIS_TACTIC_LANG: nx_int = 5 |
| 41 | const NX_AXIS_AUTO_PROVER: nx_int = 6 |
| 42 | const NX_AXIS_SEMANTIC_REJECT: nx_int = 7 |
| 43 | const NX_AXIS_LIBRARY_SIZE: nx_int = 8 |
| 44 | const NX_AXIS_LOGIC: nx_int = 9 |
| 45 | const NX_AXIS_CLASSICAL_AXIOMS: nx_int = 10 |
| 46 | const NX_AXIS_ARITH_SUBSTRATE: nx_int = 11 |
| 47 | const NX_AXIS_PROB_SUBSTRATE: nx_int = 12 |
| 48 | const NX_AXIS_PROOF_OUTPUT: nx_int = 13 |
| 49 | const NX_AXIS_OPEN_SOURCE: nx_int = 14 |
| 50 | const NX_AXIS_VISUAL_NATIVE: nx_int = 15 |
| 51 | const NX_AXIS_PHYSICS: nx_int = 16 |
| 52 | const NX_AXIS_CHEMISTRY: nx_int = 17 |
| 53 | const NX_AXIS_LINALG: nx_int = 18 |
| 54 | const NX_AXIS_SYMBOLIC_CALC: nx_int = 19 |
| 55 | const NX_AXIS_BITS_UP_BUILD: nx_int = 20 |
| 58 | const NX_VERDICT_WIN_BIG: nx_int = 1 |
| 59 | const NX_VERDICT_WIN: nx_int = 2 |
| 60 | const NX_VERDICT_TIE: nx_int = 3 |
| 61 | const NX_VERDICT_LOSE: nx_int = 4 |
| 62 | const NX_VERDICT_LOSE_BIG: nx_int = 5 |
| 63 | const NX_VERDICT_UNMEASURABLE: nx_int = 6 |
functions
| 65 | func nx_peer_name(p: nx_int) -> *u8 |
| 78 | func nx_verdict_name(v: nx_int) -> *u8 called by 1: nx_compare_row |
| 88 | func nx_axis_name(a: nx_int) -> *u8 called by 1: nx_compare_row |
| 113 | func nx_compare_row(axis: nx_int, peer: nx_int, our_val: *u8, peer_val: *u8, |