Contacts

---

Fill the callback form!

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

Curriculum Vitae & Career Dossier

(request via email if anything is inaccessible)

[PDF]	Curriculum Vitae (English)
[PDF]	Lebenslauf (German)
[PDF]	Curriculum Vitae (Russian)
[PDF]	Executive Brief (English)
[PDF]	Cover Letter Dossier
[Card]	Interactive 3D Digital Business Card ([Print PDF])
[vCard]	Electronic Contact Card (VCF format)

Repositories

• Proof Assistant "set_theory_prover" (Obelisk):
  A proof assistant for Morse-Kelley (MK) class theory and NBG foundations with a minimal trusted kernel. Semantics is strictly non-computational: the compiler statically typechecks derivations without emitting bytecode. Features verified ordinal arithmetic and formal de Bruijn export.
  

  [GitHub]	(kernel, standard library, and classical deduction engine)
  [link]	(project web presentation and dual-pane demonstration)
  [Doc]	(monograph on Quotation & Antiquotation, Shift-to-Term principle, and nested stratification)
  [Doc]	(3-Stage NBG Propositions-as-Types Compiler Blueprint: Stage I Predicative NBG, Stage II MK + Dunaev Tagged Pairs, Stage III Stratified Quotation/Antiquotation)
  [LP]	(LambdaPi / Dedukti formal proof certificate for NBG Propositions-as-Types theorems)

• Formal Foundations "draftarticle":
  Formal verification in Rocq (Coq) of classical first-order logic (soundness and completeness theorems) and ZFC set theory following Benjamin Werner's approach, developed independently from each other.
  

  [GitHub]	(source repository)
  [PDF]	(technical report on 1st order logic & ZFC implementation in RoqC)

• Mechanized Mathematics "Recursion-Addition":
  Formal mechanization in Isabelle/ZF of a general transfinite recursion theorem and foundational ordinal arithmetic.
  

  [link]	Recursion Theorem in ZF, Archive of Formal Proofs, May 2020.

• Category Theory Monograph "yoneda_ai":
  AI-assisted formal monograph and machine-checked exploration of category theory centered on the Yoneda Lemma.
  

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

• High-Assurance Methodology "antivibecoding":
  Manifesto and principles against careless "vibe coding", advocating for machine-checked specifications, zero-trust correctness, and formal verification in critical systems.
  

  [GitHub]	(manifesto, 10 inviolable laws, and verification tools)
  [HTML]	(online manifesto, slide presentation & ROI calculator)

• Autonomous Infrastructure "mybot":
  Multi-agent container orchestration platform, local GitLab API server, ticket tracking system, and automated task runner.
  

  [Gallery]	(platform interface screenshots · 5 images gallery)

  🖼️ View Platform Screenshots Gallery (5 screenshots)

  Click any screenshot to view full resolution:

  

  1. Dashboard & Telemetry

  

  2. Agent Fleet & Queues

  

  3. Blue/Green Deploy

  

  4. Cognitive Memory

  

  5. Estimations & Pace
• Curriculum Vitae Dossier "CV":
  Multi-lingual LaTeX and ReportLab CVs, cover letters, and career dossier with automated generation and validation.
  

  [GitHub]	(source repository)
  [PDF]	(curriculum vitae in English)
  [PDF]	(Lebenslauf in German)

• Personal Portal "georgydunaev.github.io":
  Personal academic and research portfolio website.
  

  [GitHub]	(source repository)
  [link]	(live site)

• Obelisk Web Portal "obeliskproofassistant.github.io":
  Public portal for the Obelisk Proof Assistant, dual-pane interactive demonstration, and Lean 4 formal audit.
  

  [GitHub]	(web source repository)
  [link]	(live portal)

• Formal Logic & Predicate Calculus "VerifiedMathFoundations":
  Mechanized proofs in Rocq (Coq) of first-order theories, deduction theorem, soundness of predicate calculus, and intuitionistic propositional logic based on Shen's mathematical logic.
  

  [GitHub]	(formal Coq developments: Deduction.v, PredicateCalculus.v, IntuitCompleteness.v)

• Set Theory Formalization "JechExercises" & "Jech":
  Machine-checked formalization in Isabelle/ZF of theorems and exercises from Thomas Jech's classic treatise Set Theory.
  

  [GitHub]	(Isabelle proof document & exercises)
  [GitHub]	(set theory theorem developments)

• Push-to-Talk Voice Room "iumvo.github.io":
  A simplest possible push-to-talk voice room web application built with WebRTC and vanilla JavaScript.
  

  [GitHub]	(source repository)
  [link]	(live voice room)

• Interactive Standard ML "tictactoe":
  Interactive terminal game engine and minimax decision procedure written in Standard ML for Poly/ML.
  

  [GitHub]	(Poly/ML SML source code)

• Compiler Research "problem_with_exceptions":
  Investigation into inheriting and extending exception translation mechanisms in CakeML verified compiler.
  

  [GitHub]	(CakeML research repository)

• Constructive Foundations "some_cubical_proofs":
  Formal constructive proofs written in Cubical Type Theory (Cubical Agda / ctt).
  

  [GitHub]	(cubical type theory formal proofs)

• Kernel Driver Optimization "wifi_rtl8723de":
  Realtek RTL8723DE Linux kernel wireless driver module patches for enhanced signal stability and antenna selection.
  

  [GitHub]	(kernel module configuration and build scripts)

Projects

• Proof assistant "Obelisk":
  

  ‼️[link]	(website for the project and other materials about the foundations of mathematics)

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

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

• Monograph "Some Proofs in Category Theory: The Yoneda Lemma" (yoneda_ai):
  AI-generated category theory monograph focused on Yoneda lemma
  

  [GitHub]	(source repository)
  [link]	(GitHub release v0.1)
  [PDF]	(the book)
  [HTML]	(online monograph summary & proofs)

• ...

AI-Generated Website Versions

The following modern interactive website versions were developed during AI-assisted programming sessions and are preserved here as alternative presentations:

• Modern Responsive Portfolio (AI Version):
  Alternative personal landing page with interactive category diagrams, dark/light theme switching, filterable research cards, and client-side search.
  

  [link]	(AI-generated portfolio landing page)
  [HTML]	(interactive SVG category theory & Yoneda diagrams)
  [Card]	(3D interactive business card)

• Obelisk Proof Assistant Portal (AI Version):
  Modern responsive landing page for Obelisk featuring the live Web REPL, formal logic comparison matrix, and Lean 4 audit documentation.
  

  [link]	(AI-generated Obelisk landing page)
  [REPL]	(interactive in-browser Obelisk proof checker)
  [Manual]	(complete ML-generated reference manual)

Publications

• Mechanisation of a recursion theorem:
  

  [link]	Recursion Theorem in ZF, Archive of Formal Proofs, May 2020.

• Declaration of the proof assistant project goals:
  

  [link]	Project: Obelisk Proof Assistant, ai4math.de, Oct 2026.

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

  [PDF]	1st order logic & ZFC implementation in RoqC, GitHub release, 2019.

• ...

Miscellaneous

• Outdated personal page:
  

  [link]	(very old descriptions of my GitHub repositories)

Research

Software development, testing, formal verification, functional programming languages, compilers, proof assistants.