Introduction
The Obelisk Proof Assistant is an experimental project exploring a new approach to formal mathematics, proof assistants, and programming-language design.
The project has three closely connected goals:
- developing a new proof assistant for representing and checking mathematical proofs;
- developing a programming language designed around the needs of formal reasoning;
- exploring a reformulation of classical class-theoretic foundations of mathematics.
The broader aim is to investigate how mathematical knowledge can be represented in a form that is both accessible to humans and suitable for machine manipulation and automated reasoning.
Main content
Obelisk is intended as an experimental environment for investigating the boundary between programming languages, formal mathematics, and automated theorem proving.
A central motivation is that a proof assistant should not only serve as a verifier of already-written proofs, but should also provide a useful representation of mathematical knowledge that can be manipulated, searched, transformed, and potentially used by AI systems for mathematical reasoning.
The project therefore explores:
- formal representation and verification of mathematical statements;
- a dedicated language for expressing mathematical structures and proofs;
- alternative approaches to foundational and class-theoretic representations;
- interaction between human-written mathematics and machine-generated formal proofs;
- interoperability with existing proof-assistant ecosystems where useful.
The project is currently experimental and exploratory rather than presented as a finished replacement for established systems such as Lean, Coq, Isabelle, or Agda. Its purpose is to investigate whether different design choices can provide useful advantages for formal mathematics and AI-assisted reasoning.
The project website contains demonstrations and further technical material:
Obelisk Proof Assistant — obeliskproofassistant.github.io
Relevance to AI4Math
Obelisk is relevant to AI4Math because proof assistants provide a precise computational representation of mathematical reasoning. Such representations can serve as a foundation for automated theorem proving, proof generation, verification, and AI-assisted mathematical research.
The project is particularly interested in the possibility of combining formal proof infrastructure with machine reasoning: mathematical statements can be represented formally, candidate proofs can be generated or transformed computationally, and the resulting proofs can be checked by a formal system.
The project is therefore intended as experimental infrastructure for exploring how programming languages, proof assistants, mathematical foundations, and AI-based reasoning can interact.
Current status
Obelisk is an ongoing research and development project. The public project website provides demonstrations and technical documentation, and the project is intended to evolve through experimentation and comparison with existing approaches to formal mathematics and theorem proving.