𝒲, ℰ, 𝒯, ℱ), and the explicit typed term interpretation μA. Please use the live AI portal obelisk_ai.html and the canonical Poly/ML-generated portal generated/index.html.
Obelisk is an interactive proof assistant engineered for mathematical clarity and high assurance. Featuring an audited LCF-style trusted kernel in Standard ML, declarative syntax, and rigorous class theory foundations.
Every statement is formally decoupled into Morse–Kelley Semantic Objects and Ambient Type-Theoretic Syntactic Side Conditions. Each theorem and rule links to an individual machine-checked verification certificate with full PolyML microkernel proof programs.
In standard ZFC and dependent type systems (Lean 4, Coq), collections like the universal class \(V\) or the category of all sets \(\mathbf{Set}\) cannot be manipulated as ordinary elements without triggering Russell's paradox or ascending into infinite universe hierarchies (Type u).
Obelisk adopts Morse–Kelley (MK) class theory: proper classes are native first-class objects with full impredicative comprehension over classes.
Standard Kuratowski pairs \(\langle A, B \rangle = \{\{A\}, \{A, B\}\}\) fail for proper classes because proper classes cannot be elements of sets. Obelisk solves this via Dunaev Tagged Pairs \([A, B]_D = \mathrm{mark}(A, 1) \cup \mathrm{mark}(B, 2)\), allowing proper classes and infinite families to form pairs and lists with minimal rank growth and full algebraic projection injectivity.
Type-theoretic proof assistants suffer from fragile computational reduction (\(\beta\delta\iota\)): definition updates break proof scripts invisibly. Obelisk separates syntax from semantics through the explicit valuation bracket \(\llbracket \cdot \rrbracket\). Every deduction is a checkable syntactic tree; inference rules have explicit side conditions with no hidden normalization noise.
The prover and its generated manual are continuously re-audited. These are the latest changes now visible in the Theory Manual and the publication PDFs.
[A,B]D = [C,D]D → A = C ∧ B = D is now proved for arbitrary classes
(proofDunaevPairInjectivity and surface dunaev_pair_injective).
The general Pair/Func interface no longer falls back to Kuratowski pairs.
ThmWithPrf.cheat now raises, and derive, check,
slow_check, and checkPlus all reject PCheat_prf.
Unsupported legacy PS1_prf/PHenkin_prf constructors fail explicitly. A closedness gate also rejects theorem statements with free class variables, so an open formula cannot be packed as a Set witness.
The dependent catalog now reports 42 derived proofs, 16 conservative definitions, and 7 irreducible MK axioms. Plan witnesses are classified, and an unclassified witness prevents the catalog from loading.
Inspect the catalog →
All 17 machine-checked NBG surface theorems are now rendered as a manual appendix,
including Dunaev pair injectivity and Cartesian-product elimination (dunaev_cartesian_elim), with formulas, proof AST sizes,
and normalized sizes. The same table is included in the publication PDFs.
Toggle between formal mathematical notation (Unicode / LaTeX) and concrete executable SML/Obelisk syntax. Side conditions are made fully visible and explicit.
Significantly reduces the steep learning curve for working mathematicians.
Eliminates opaque tactic noise (intro, apply, rewrite) and normalisation tricks.
Every proof step forms an explicit, checkable syntactic tree without hidden reduction steps.
Constructs a new high-assurance language with full polymorphism (types depending on values) by introducing a clean abstraction and code-generation layer above the verified CakeML compiler.
Modernized Morse–Kelley (MK) class-theoretic foundations equipped with Tarski–Grothendieck universes, regularity via powerclasses (∈-induction), and an innovative independent construction of tagged pairs and lists for proper classes.
In Obelisk, we establish a strict 1-to-1 Curry–Howard correspondence between mathematical theorems of Morse-Kelley (MK) Impredicative Class Theory and compiler types. Because MK allows quantification over proper classes in class comprehension, it provides the full expressive strength of higher-order logic over sets, while the compiler operates under the foundational principle: it compiles not to generate runtime executable bytecode, but strictly to verify whether the proof expression type-checks.
Eliminates dynamically typed languages like Python from the trusted kernel. Fully written in Standard ML 97 targeting the CakeML verified compiler for machine-code assurance down to silicon.
Every mathematical theorem (Modus Ponens, Conjunction Symmetry, Russell Paradox Refutation) corresponds to a unique type. Proof terms are formal witnesses checked by the SML type checker.
Replaces Kuratowski pairs (which collapse on proper classes) with [A, B]_D tagged pairs that preserve well-foundedness and algebraic projections without universe elevation.
Validates all 49 core proof certificates and NBG standard library theorems in <50 MB RAM under Poly/ML & CakeML or zero-install browser JS, contrasting with multi-gigabyte JVM/LSP heaps.
| Surface Declaration | Kernel AST Category | Example in .nbg Surface Language |
Checked by NBGCompiler.typeCheck |
Epistemic Meaning |
|---|---|---|---|---|
formula F = ...; |
Type Definition (Fm / NBGCompiler.Type) |
formula False_RussellIsSet = Set({ x | x in x -> Bot }); |
Verifies syntactic well-formedness & Stage I/II quantifier bounds | Defines a proposition (Type) — even a false/uninhabited one. Never proves a theorem! |
theorem T : F = e; |
Proof Term (NBGCompiler.Expr) |
theorem thm_russell_not_set : Set(R) -> Bot = fn (hSet : Set(R)) => ...; |
Synthesizes exact type of term e via NBGCompiler.typeCheck and verifies α-equivalence with F |
Constructive witness inhabiting type F. Uninhabited/false formulas are deterministically rejected. |
| System | Logical Foundation | Proof Execution | Trusted Kernel | Mathematical Workflow |
|---|---|---|---|---|
| Obelisk | Morse–Kelley Class Theory + Tarski Universes | Zero Implicit Computation (Syntactic Trees) | Small LCF Kernel (~20k LOC SML) | Declarative, human-readable, stable under definition updates |
| Lean 4 | Calculus of Inductive Constructions (CIC) | Type reduction, unification, tactic elaboration | Complex C++ kernel + elaborator | Tactic-heavy, dependent types, steep learning curve |
| Rocq (Coq) | Calculus of Inductive Constructions (CIC) | Computational reduction (β, ι, δ) | OCaml kernel (~30k LOC) | Constructive type theory, Ltac scripting |
| Isabelle/ZF | ZFC over Higher-Order Logic (Isabelle/Pure) | Term rewriting, tableau provers, Sledgehammer | Standard ML LCF kernel | Isar declarative proofs, Isabelle framework |
| Metamath | First-Order Logic + Set Theory (ZFC) | Pure syntactic replacement & verification | Minimalist (~1k LOC) | Very low-level, lacks higher polymorphism & reflection |
The Obelisk system axiomatics and independent constructions (including Dunaev tagged pairs & lists) were audited and machine-checked in Lean 4. All core theorems were verified with 0 errors and 0 sorry.
Live demonstration of Obelisk proofs, axiomatics, and mathematical derivations directly from the kernel.
