Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt

Use this file to discover all available pages before exploring further.

Lean-Spec is a hands-on tutorial demonstrating how to use Lean 4 as a formal program specification language. By leveraging dependent types and the propositions-as-types correspondence, you can express exactly what a function must achieve — not how it achieves it — with mathematical precision and no ambiguity.

Introduction

Understand why formal specification matters and how Lean 4 uniquely supports it

Quickstart

Write your first Lean 4 specification in minutes

Core Concepts

Learn types, propositions, subtypes, and dependent types

Examples

Walk through worked specifications from classic computing problems

​
Why Lean for Specification?

Natural language requirements are open to interpretation. Lean specifications are not. Using Lean’s dependent type system, you can:
  • Embed constraints directly into types — a FlightDeparture type that structurally cannot have an empty runway set
  • Express preconditions and postconditions as first-class types, not comments
  • Catch specification errors early — an unimplementable spec fails to type-check, just like a bad theorem fails to prove
  • Share one language across specification, implementation, and proof — no translation layer

​
Tutorial Structure

Lean as a Spec Language

Overview of Lean logic, types, and the specification workflow

Types and Propositions

How propositions and types relate and why it matters for specs

Subtypes and Dependent Types

The core tools for embedding constraints in specifications

Quotient & Remainder

A simple example illustrating subtype-based specification

Sorting

Specifying sort correctness with ordered and permutation predicates

Knapsack

Specifying optimisation problems: characterise solutions, not algorithms

Graph Search

Paths, shortest paths, and handling non-existence with sum types

Aviation Scheduling

A real-world departure TMI specification from the aviation industry

​
Reference

Support Libraries

Utility types, temporal definitions, and geospatial primitives

Flight Planning Modules

ICAO flight planning message processing — a full industry-scale specification

Build docs developers (and LLMs) love

Get started for freeTalk to us