Publications and Research Projects

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. ...

Gödel’s Poetry is a Lean 4 theorem proving project that combines AI-based proof generation with recursive decomposition, retrieval-augmented theorem search, and verifier-guided proof reconstruction. The project explores how modern language models, formal proof assistants, and multi-agent architectures can work together to prove mathematical statements in Lean. Key components include: Lean 4 proof generation recursive theorem decomposition RAG-based theorem retrieval AST-based subgoal extraction proof verification via Lean tooling GitHub repository Related blog post: ...

We welcome contributions from the community. If you are working on a project or have a publication related to AI and mathematics, you can feature it here. This includes, for example: research papers software projects (e.g. GitHub repositories) teaching materials experimental or exploratory work To submit your contribution, please use the submission form: Submit your contribution We encourage concise and well-structured descriptions so that others can quickly understand and engage with your work. ...