Obelisk Proof Assistant — Strictly ML-Generated Artifacts Directory (generated/)

Every file in obeliskproofassistant.github.io/generated/ is emitted exclusively by Standard ML scripts in set_theory_prover/program/ (User Directive #17).

Formula Display:
Proof Trees:

ML-Generated Output Registry (18 Primary Artifacts + 106 Standalone Entry Pages + 124 Personal Symbol Pages)

AI processes are strictly forbidden to edit any file inside generated/ directly; all outputs are produced by running poly -q --use html_generator.ML and poly -q --use nbg_html_generator.ML.

ID Generated Artifact Record (Vertical Field Table)
01
Artifact generated/manual.html — Complete Entity Database (1.01-5.02)
Format HTML Catalog
ML Provenance html_generator.ML <- newchecker.ML
Description All 106 1st-order kernel axioms, inference rules, definitions, and theorems with clickable Unicode & LaTeX formulas.
02
Artifact generated/variant1.html — Variant 1: 1st-Order Syntactical Proof Assistant (MKTD1)
Format HTML Catalog
ML Provenance html_generator.ML <- newchecker.ML
Description Dedicated Variant 1 reference catalog (Fm, Stmt, Ctx, Theory, Prf, Class).
03
Artifact generated/variant2.html — Variant 2: Higher-Order MKTD2 Formulas-as-Types
Format HTML Catalog
ML Provenance nbg_html_generator.ML <- verified_theorems.ML
Description Dedicated Variant 2 reference catalog (100 mechanically type-checked records: 77 Derived + 16 Definitions + 7 Axioms).
04
Artifact generated/nbg_library.html — Variant 2 MKTD2 Library Catalog
Format HTML Catalog
ML Provenance nbg_html_generator.ML <- verified_theorems.ML
Description Complete Variant 2 constructive lambda-term library with proof term sizes and clickable formulas.
05
Artifact generated/proofs.html — Verified Theorems & Inference Rules Gallery
Format HTML Catalog
ML Provenance html_generator.ML <- newchecker.ML
Description Filtered gallery of all kernel-verified theorems and primitive/derived inference rules.
06
Artifact generated/dependent_types.html — Dependent Types, Families, Sigma/Pi & Universes
Format HTML Catalog
ML Provenance html_generator.ML <- newchecker.ML
Description Dependent types, families, Sigma/Pi, cardinals, and Grothendieck-Tarski universes ordered via types/order_dependent_types.txt.
07
Artifact generated/metatheory.html — Metatheory, Explicit Substitution & Incompleteness
Format HTML Catalog
ML Provenance html_generator.ML <- newchecker.ML
Description Reflection, explicit substitution, and incompleteness entries ordered via types/order_metatheory.txt (4.01-4.06 and 5.01-5.02).
08
Artifact generated/symbols.html — Algorithmic Symbol, Operator & Type Registry
Format HTML Catalog
ML Provenance html_generator.ML
Description Complete registry of hyperlinked symbols, operators, connectives, predicates, and kernel types.
09
Artifact generated/symbols/index.html — Personal Symbol Reference Pages (Quotation, Antiquotation, Encoding, Embedding, Interpretation, Types & Binders)
Format HTML Directory
ML Provenance html_generator.ML
Description 124 standalone personal reference pages under generated/symbols/<slug>.html explaining the mathematical semantics of quotation/antiquotation, Enc/Dec, Emb, mu_A, Class, binders, and dependent conditionals in MKTD1 and MKTD2.
10
Artifact generated/proofs/index.html — Individual Entity & Certificate Pages (1.01-5.02)
Format HTML Directory
ML Provenance html_generator.ML <- newchecker.ML
Description Index of 106 standalone entity pages under generated/proofs/<Name>.html.
11
Artifact generated/sections/sec-1.html — Section 1: Propositional Logic (1.01-1.14)
Format HTML Section
ML Provenance html_generator.ML <- newchecker.ML
Description Standalone Section 1 catalog page.
12
Artifact generated/sections/sec-2.html — Section 2: Predicate Logic (2.01-2.06)
Format HTML Section
ML Provenance html_generator.ML <- newchecker.ML
Description Standalone Section 2 catalog page.
13
Artifact generated/sections/sec-3.html — Section 3: Set/Class Foundations (3.01-3.78)
Format HTML Section
ML Provenance html_generator.ML <- newchecker.ML
Description Standalone Section 3 catalog page.
14
Artifact generated/sections/sec-4.html — Section 4: Metalogical Laws (4.01-4.06)
Format HTML Section
ML Provenance html_generator.ML <- newchecker.ML
Description Standalone Section 4 catalog page.
15
Artifact generated/sections/sec-5.html — Section 5: Incompleteness Statements (5.01-5.02)
Format HTML Section
ML Provenance html_generator.ML <- newchecker.ML
Description Standalone Section 5 catalog page.
16
Artifact generated/theory_db.json — Variant 1 Machine-Readable Entity Database
Format JSON Export
ML Provenance html_generator.ML <- newchecker.ML
Description 106 kernel entries with Unicode, SML Kernel AST, HTML-linked Unicode, and hyperlinked LaTeX fields.
17
Artifact generated/nbg_library.json — Variant 2 Machine-Readable MKTD2 Library
Format JSON Export
ML Provenance nbg_html_generator.ML <- verified_theorems.ML
Description 100 type-checked MKTD2 records in structured JSON format.
18
Artifact generated/output.txt — Plain-Text Kernel Entity Database
Format Plain Text
ML Provenance html_generator.ML <- newchecker.ML
Description Clean plain-text dump of all 106 entries (1.01-5.02).