⭐ Starling
Starling is a proof assistant that makes interactive theorem proving accessible.
⭐ Try Starling Now
No installation needed! Open the web editor and try writing a proof in the Starling language.
⭐ Quick Start
In your terminal:
git clone https://github.com/starlinglang/starling.git
npm install
cd starling/ide
npx http-server
⭐ Features
Starling is inspired by the simplicity of Metamath and the readability of Isabelle/Isar, inheriting Metamath's proof verifier and Isabelle/Isar's readable grammar.
⭐ Why Starling?
The learning curve for existing proof assistants is steep, and the error messages given are not always helpful.
Starling is a rigorous proof assistant which is meant to be friendly to mathematicians and students at the beginning of their coding journey.
⭐ Contributing
The build system for this project is relatively simple:
git clone https://github.com/starlinglang/starling.git
npm install
npm run build
If you want to contribute, you might consider working on these features.