The formal source

Inspect Lean

Read the code behind the papers. Find a file, explore its declarations, and link directly to the source.

20 reading editions2722 source files

Coverage labels describe the existing evidence. Browsing the source does not run Lean.

Open the Lean workspace Compiler runs in this browser · 17 prepared workspaces

Run with dependencies All displayed source files · native Lean

Core papers

Books and monographs