⭐ 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

Contributions are welcome!

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.