nx_autoformalize.nx source
↩ module page · 94 lines · 6008 B
1// nx_autoformalize.nx -- AUTOFORMALIZATION rungs 1-4: informal arithmetic claim -> FORMAL Peano terms -> a
2// derivation CHECKED by the LCF-style v2 kernel. This is the computational Frontier Radar's number-one
3// OPPORTUNITY (momentum 33, researcher-measured 2025/26: autoformalization / proof assistants) getting its
4// first sovereign organ -- the census found the gap, this closes rungs 1-4.
5//
6// 2026-07-15: the af_* machinery moved VERBATIM to nx_autoformalize_lib.nx (pure lib, no main) so other
7// organs can compose the verifier -- the propose->verify loop (nx_nofloat_propose_verify_gate: the no-float
8// LLM proposes, this kernel disposes). This organ = the same battery over the lib; behavior unchanged and
9// re-proven by the battery below.
10//
11// SCOPE (honest): "<n|what> [plus|times <n|what>] =|<|<= <n>" (digits or number-words zero..twelve). A FALSE
12// claim ("2 + 2 = 5") formalizes but is REFUTED; out-of-grammar text -> UNSUPPORTED (honest, no guess). The
13// frontier meaning of autoformalization is LLM->Lean at paper scale -- this is rungs 1-4 of that ladder.
14// Modes: no-arg = gate battery (expect_exit 0); argv[1] = one informal claim -> verdict.
15// license_tier: ORIGINAL expect_exit: 0
16import "nx_autoformalize_lib.nx"
17
18func main(argc: i64, argv: *i64) -> i64 {
19 if argc >= 2 {
20 let r: i64 = af_decide(argv[1] as *u8, 1)
21 if r == 1 { sys_exit(0); return 0 }
22 sys_exit(1)
23 return 1
24 }
25 af_w("=== NX-AUTOFORMALIZE rungs 1-4 -- informal arithmetic (plus, times, orderings, solve-forms) -> Peano terms -> kernel-checked derivation ===\n" as *u8)
26 var pass: i64 = 0
27 var fail: i64 = 0
28 // T1..T4: true claims in both surface forms must PROVE
29 if af_decide("2 + 2 = 4" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
30 if af_decide("two plus three equals five" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
31 if af_decide("7 + 0 = 7" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
32 if af_decide("twelve plus twelve equals 24" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
33 // T4b..T4d rung 2: MULTIPLICATION claims (each mult step composes a full rung-1 plus proof)
34 if af_decide("2 * 3 = 6" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
35 if af_decide("three times four equals twelve" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
36 if af_decide("5 * 0 = 0" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
37 if af_decide("six times six equals 36" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
38 // T4e..T4h rung 3: ORDERING claims (< / <= via exists-witness definitional instances + REFL for le-equal)
39 if af_decide("4 < 5" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
40 if af_decide("2 + 2 < 5" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
41 if af_decide("7 <= 7" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
42 if af_decide("two times three is under 7" as *u8, 1) == 1 { pass = pass + 1 } else { fail = fail + 1 }
43 // T4i..T4l rung 4: SOLVE-FORMS (one unknown, eq-only; answer + kernel certificate)
44 var sol_ok: i64 = 0
45 if af_decide("what plus 3 equals 7" as *u8, 1) == 1 { sol_ok = sol_ok + 1 }
46 if af_decide("3 plus what equals 7" as *u8, 1) == 1 { sol_ok = sol_ok + 1 }
47 if af_decide("what times 4 equals 12" as *u8, 1) == 1 { sol_ok = sol_ok + 1 }
48 if af_decide("x * 5 = 0" as *u8, 1) == 1 { sol_ok = sol_ok + 1 }
49 // T4m/T4n rung 4: honestly NO-SOLUTION over the naturals
50 var nosol_ok: i64 = 0
51 if af_decide("what times 4 equals 13" as *u8, 1) == 5 { nosol_ok = nosol_ok + 1 }
52 if af_decide("what plus 9 equals 7" as *u8, 1) == 5 { nosol_ok = nosol_ok + 1 }
53 // T5 NEG-CONTROL: a FALSE claim must be REFUTED (formalizes fine, does NOT prove)
54 var neg_ok: i64 = 0
55 if af_decide("2 + 2 = 5" as *u8, 1) == 2 { neg_ok = 1 }
56 // T5b NEG-CONTROL (mult): false product must be REFUTED
57 var neg2_ok: i64 = 0
58 if af_decide("2 * 3 = 7" as *u8, 1) == 2 { neg2_ok = 1 }
59 // T5c/T5d NEG-CONTROLS (orderings): false relations must be REFUTED
60 var neg3_ok: i64 = 0
61 if af_decide("5 < 3" as *u8, 1) == 2 { neg3_ok = 1 }
62 var neg4_ok: i64 = 0
63 if af_decide("2 + 2 <= 3" as *u8, 1) == 2 { neg4_ok = 1 }
64 // T6 honesty: out-of-grammar input must be UNSUPPORTED, never guessed
65 var unsup_ok: i64 = 0
66 if af_decide("the moon is made of cheese" as *u8, 1) == 3 { unsup_ok = 1 }
67 af_w(" TALLY: proved " as *u8); af_n(pass); af_w("/12 solved " as *u8); af_n(sol_ok); af_w("/4 no-solution-honest " as *u8); af_n(nosol_ok); af_w("/2 neg-refuted " as *u8); af_n(neg_ok + neg2_ok + neg3_ok + neg4_ok); af_w("/4 unsupported-honest " as *u8); af_n(unsup_ok); af_w("/1\n" as *u8)
68 let liar_pass: i64 = (pass == 12) as i64
69 let liar_sol: i64 = (sol_ok == 4) as i64
70 let liar_nosol: i64 = (nosol_ok == 2) as i64
71 let liar_negf: i64 = (fail == 0) as i64
72 af_w(" LIAR-KILL: all-true-proved=" as *u8); af_n(liar_pass)
73 af_w(" false-plus-refuted=" as *u8); af_n(neg_ok)
74 af_w(" false-mult-refuted=" as *u8); af_n(neg2_ok)
75 af_w(" false-lt-refuted=" as *u8); af_n(neg3_ok)
76 af_w(" false-le-refuted=" as *u8); af_n(neg4_ok)
77 af_w(" out-of-grammar-honest=" as *u8); af_n(unsup_ok)
78 af_w(" solve-forms=" as *u8); af_n(liar_sol)
79 af_w(" no-solution-honest=" as *u8); af_n(liar_nosol)
80 af_w(" no-true-claim-failed=" as *u8); af_n(liar_negf); af_w("\n" as *u8)
81 var ok: i64 = liar_pass & neg_ok
82 ok = ok & neg2_ok
83 ok = ok & neg3_ok
84 ok = ok & neg4_ok
85 ok = ok & liar_sol
86 ok = ok & liar_nosol
87 ok = ok & unsup_ok
88 ok = ok & liar_negf
89 af_w("NX-AUTOFORMALIZE verdict=" as *u8)
90 if ok == 1 { af_w("GREEN -- informal claims formalized to Peano terms and derived through the LCF kernel; false claim refuted; out-of-grammar honest\n" as *u8); sys_exit(0); return 0 }
91 af_w("RED\n" as *u8)
92 sys_exit(1)
93 return 1
94}