Greetings

This site contains a demonstration of the development of a proof assistant, as well as various related links, texts, presentations, and materials about the foundations of mathematics.

The project aims to achieve three results:

• a new proof assistant with significantly reduced learning curve and bidirectional communication with mathematical community: it doesn't require a user to learn additional information about term normalisation, foundations, tactics, and many others notions, which are typically unusual for a mathematician to know;
• a new programming language with certain nice properties(e.g.: better polymorphism) via adding additional abstract layer on compiler of the existing project CakeML;
• "refactored", but still traditional class-theoretic foundations of mathematics.

Resources

• Personal page of the author:
  

  [link]	‼️click here‼️

• Proof assistant "Obelisk":
  

  [HTML]	(full-screen demonstration)
  [PDF]	(verified demonstration · dark background)
  [PDF]	(verified demonstration · light ink-saving background)

• Declaration of the proof assistant project goals:
  

  [link]	(on the site ai4math.de)

• Monograph "Class-Theoretic Foundations of Mathematics":
  Unfinished 200-page document.
  

  [PDF]	(a draft is currently availble only via request by email)

• Embeddings of classical 1st order logic (including soundness and completeness theorems done for slightly different Rocq (Coq)-specific semantics) and ZFC theory (following Werner's approach) in Rocq (formerly Coq), both done independently from each other via two different techniques:
  

  [PDF]	1st order logic & ZFC implementation in Rocq (Coq), GitHub release, 2019.

• Algorithmically generated entity database (Definitions, Axioms, Rules, Theorems):
  

  [HTML]	(Standard ML kernel-generated manual with algorithmic symbol & type links)
  [NBG]	(Standard ML kernel-generated 100-theorem NBG Formulas-as-Types catalog)
  [Proofs]	(Standard ML kernel-generated verified theorems & inference rules gallery)
  [JSON]	(Machine-readable entity database exported directly from newchecker.ML)

• Formal Foundations & Machine-Checked Dossiers:
  

  [Doc]	Ordinal Arithmetic Theorems: step-by-step constructive derivations of all 12 ordinal theorems in Morse-Kelley class theory.
  [Doc]	Proof of Ord(On): detailed slide walkthrough and formal verification in the Obelisk dependent compiler.
  [Doc]	Non-Computational Semantics: specification of the static verification compiler (pure derivation checking without bytecode emission).
  [Doc]	Quotation & Antiquotation: deep mathematical analysis of the Shift-to-Term principle, nested stratification, valuation under unnamed assignments, and non-computational semantics.
  [Doc]	3-Stage NBG Propositions-as-Types Architecture (Argon Blueprint): Stage I predicative NBG, Stage II MK + Dunaev tagged pairs, and Stage III Tarski-stratified 2-stage Quotation & Antiquotation.
  [LP]	LambdaPi / Dedukti Proof Certificate: independently verifiable LF proof terms exported from the NBG Propositions-as-Types compiler.
  [SML]	Obelisk Unfolded Monolith: self-contained single-file Standard ML compiler (19 SML structures including VariantBridge, compiles with Poly/ML 5.7.1 & CakeML, 0 external dependencies).
  [Doc]	Two Proof Assistant Variants & Dual Semantics of typetheory.ML: Variant 1 (1st-Order NBG/MK with Option B 7-part Stmt/Enc/Dec/Emb/ProofsOf/Theorems anatomy) and Variant 2 (Higher-Order Formulas-as-Types), linked by VariantBridge.

• Monograph "Some Proofs in Category Theory: The Yoneda Lemma" (yoneda_ai):
  AI-generated category theory monograph and machine-checked exploration centered on the Yoneda Lemma.
  

  [GitHub]	(source repository)
  [link]	(GitHub release v0.1)
  [PDF]	(the monograph PDF)
  [HTML]	(online monograph summary & Yoneda embedding notes)

• AI-Generated Modern Landing Pages:
  Alternative modern web pages developed during AI-assisted programming sessions:
  

  [link]	(AI-generated Obelisk responsive landing page)
  [REPL]	(interactive in-browser typechecker & deduction engine)
  [Manual]	(complete ML-generated reference manual)
  [Portfolio]	(AI-generated personal research portfolio)

• Methodology & Critical Verification: "Anti-Vibe Coding":
  

  [link]	(manifesto, 10 inviolable laws, verification ROI calculator & slides)
  [GitHub]	(source repository)

Miscellaneous

This section contains AI-generated documents.

• External archival documents:
  

  [PDF]	Original machine-checked analysis draft in Russian, made by Alexey Komissarov using Claude (Fable 5).

• Presentations "Antivibecoding" (WIP):
  

  [ODP]	(slide deck presentation about the goals of the project)
  [HTML]	(AI-generated presentation about the goals of the project)

Contacts

---

Fill the callback form!

Name:		(optional)
Phone:		(optional)
Email:		(optional)
Message:		(optional)
	Submit

Acknowledgements

Geography of the site visitors