nx_mizar_ingest.nx

nx_mizar_ingest.nx -- ingest Mizar .miz theorem-level statements (M0). Mizar's syntax for declarations we track: theorem :: label <statement> proof <proof script> end; definition let ... ; func ... ; ... end; scheme :: label <scheme body> end; notation / registration / reservation -- skipped at M0 MML identifier construction: ARTICLE = uppercase filename without .miz Each theorem gets a sequential number; identifier = ARTICLE:th N Each definition gets ARTICLE:def N Each scheme gets ARTICLE:sch N We do NOT parse Mizar's typed FOL. We do NOT verify proofs. At M0, we extract the identifier list with stable QED-format names. At M1+ we'll parse statements and feed them through nx_prover. genealogy_id: trybulec_mizar_1972 + bancerek_mml + wiedijk_qed_1994 lineage_id: formal_statement_parsing + typed_fol axioms: NX_AX_ZFC_SEPARATION