Saphyra: the Beginning
A few years earlier I started developing Saphyra for fun (called Saphira then). My main goal was to build a simple proof assistant with a minimal kernel supporting multiple theories. I wanted to see how hard it was, both to build a proof assistant and to write proofs in it.
I restarted the project last year after a three-year hiatus, out of a desire to occupy myself with side projects on weekends. It's a “big clean problem” — one with a very clear goal, plenty of challenges, and an abundance of learning and experimenting opportunities.
Saphyra aims to be a proof assistant, similar to Mizar, HOL, and Coq. The program helps the user to write formal proofs of mathematical theorems that can be automatically verified, and the proof-writing process is also aided by some level of automation.
I aim to make Saphyra …
- lean:
- The kernel — the program that checks the validity and rigor of proofs — should not exceed 1000 lines of code. The more code you have, the harder it is to verify its correctness.
- extensible:
- The system should be easy to extend to support a wide range of logics: classical, intuitionistic, modal, linear; first-order, second-order, higher-order; set theories, type theories, category theories; and other user-defined systems of reasoning.
- meta:
- The system should be able to prove relations between theories, such as that any EFA theorem is also a PRA theorem, and that ZFC proves the consistency of PA. To do this, we would use a relatively weak theory (such as EFA, PRA, PA, or ZF minus ∞) to show how proofs may be converted between theories.
- easy to use:
- Usability may be improved many ways: using a familiar (Python- or Java-like) syntax; providing analysis tools; training AIs to observe common patterns in proofs; and many others.
Saphyra is hosted on GitHub; stay tuned!