Greetings

This site contains a demonstration of development of a proof assistant, which is in the viewport on the right(scrollable both up and down), as well as various related links, texts, presentations, and materials about foundations of mathematics.
Three results may be achieved:

• a new proof assistant,
• a new programming language with certain nice properties,
• "refactored" classical class-theoretic foundations of mathematics.

Resources

• A personal page of the author:
  

  [link]

• Proof assistant "Obelisk":
  

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

• A proof assistant project goals declaration:
  

  [link]

• Monography "Class-Theoretic Foundations of Mathematics":
  Unfinished 200-pages document.
  

  [PDF]

  (request via email)

Miscellaneous

• ‼️ Independent analysis of Obelisk: formalization of statements, and automatically generated compilable proofs for the LEAN proof assistant, made by Claude(Fable 5):
  

  [PDF]

  (slightly outdated, but very informative)

• Presentations "Antivibecoding"(WIP):
  

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

Contacts

Acknowledgements