A proof assistant for the mathematician.
An interactive theorem prover designed for mathematical intuition, not just programming expertise.
A Language for Insight
Starling is a high-level proof assistant for mathematicians that makes it easier to formalize math proofs without a background in computer science. Built on top of Norman Megill's Metamath and inspired by the elegance of Rust, the Starling language offers a syntax that feels more natural to the human mind.
Designed for your workflow
From undergraduate studies to advanced faculty research, Starling provides an environment for verifying your most complex conjectures.
Structured Code Editor
The Starling code editor provides real-time linting and structural guidance, ensuring your formalizations remain clean and logically sound. By prioritizing the structural hierarchy of proofs, Starling allows you to focus on the mathematics rather than the syntax.
Metamath Core
Built on the minimalist Metamath framework, Starling inherits a foundation of trust and decades of verified mathematics. It is a bridge between the rigor of computer-assisted proof and the elegance of human thought.
Infinite Canvas
Organize your files across a non-linear workspace that mirrors the way you actually think about problems. No more hunting through tabs; just a vast, intuitive space for discovery.
The Starling Language
Experience a language inspired by Rust's clarity, optimized specifically for the needs of the modern interactive theorem prover. Starling syntax is designed to be readable as pen-and-paper proofs while maintaining the strictness required for formal verification.