Verso
Verso
Written in Lean. Checked by Lean.
Verso is a platform for writing documents, books, course materials, and websites with Lean. Every code example is type-checked. Every rendered page is interactive. And it's all built on the tools you already use.
Get Started
User Manual
The type of all predicates over a type is that type's _powerset_. Elements of one of these subsets satisfy the predicate:
```lean
def Set (α : Type u) : Type u :=
α → Prop
instance : Membership α (Set α) where
mem xs x := xs x
```
A function $`f` is surjective if each element of the range is covered by an element of the domain:
```lean
def Surjective (f : α → β) :=
∀ y, ∃ x, f x = y
```
:::theorem "Cantor"
Given a function $`f ∈ S → \mathcal{P}(S)`, [Cantor's diagonal argument](https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument) involves the diagonal set $`\{x ∈ S \mid x \not\in f(x)\}`. The {tactic}`grind` tactic takes care of many reasoning steps:
```lean
theorem cantor (f : S → Set S) : ¬ Surjective f := by
intro h
have ⟨x, p⟩ := h (fun x : S => x ∉ f x)
have : x ∈ f x ↔ x ∉ f x := by
constructor <;>
simp [Membership.mem] at * <;>
grind
grind
```
:::The type of all predicates over a type is that type's powerset. Elements of one of these subsets satisfy the predicate:
def Set (α : Type u) : Type u :=
α → Prop
instance : Membership α (Set α) where
mem xs x := xs x
A function f is surjective if each element of the range is covered by an element of the domain:
def Surjective (f : α → β) :=
∀ y, ∃ x, f x = y
Given a function f ∈ S → \mathcal{P}(S), Cantor's diagonal argument involves the diagonal set \{x ∈ S \mid x \not\in f(x)\}. The grind tactic takes care of many reasoning steps:
theorem cantor (f : S → Set S) : ¬ Surjective f := S:Type u_1f:S → Set S⊢ ¬Surjective f
S:Type u_1f:S → Set Sh:Surjective f⊢ False
S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ False
have : x ∈ f x ↔ x ∉ f x := S:Type u_1f:S → Set S⊢ ¬Surjective f
S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ x ∈ f x → ¬x ∈ f xS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ ¬x ∈ f x → x ∈ f x S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ x ∈ f x → ¬x ∈ f xS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ ¬x ∈ f x → x ∈ f x
S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x x → f x x S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x xS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x x → f x x
All goals completed! 🐙
All goals completed! 🐙
Interactive
Verso files are Lean files. While writing, you get the full IDE experience, including autocomplete, error checking, go-to-definition, and tactic states. Readers get the same richness: rendered pages include proof states, hover information, and clickable links to documentation.
Correct
Verso helps you catch mistakes while writing, not after publishing. Every code example is checked by Lean as part of the build. If a described behavior doesn't match reality, you find out immediately. The Lean Reference Manual uses this to stay up to date with the latest developments.
Integrated
Built on Lean and Lake. Verso uses a lightweight Markdown-like markup language with a built-in extension mechanism. Extensions are ordinary Lean functions, not a separate plugin system or templating language. Syntax highlighting uses Lean's actual parser, so it's always accurate.
What Can You Build?
Verso's provides a shared foundation for rendering, cross-referencing, and code integration, without requiring a single core model that only really fits one kind of document. Different kinds of documents are called genres. Each genre builds on common infrastructure, so improvements to one benefit all, and anyone can implement a new genre.
Reference Manuals
Comprehensive API and language documentation
Course Notes & Textbooks
Structured educational material with worked examples
Websites & Blogs
A static site generator for project homepages, landing pages, and blog posts with integrated Lean code
Mathematical Blueprints
Plans for large-scale formalization projects
Your Document Here
Verso's genre system is extensible: you can define new document types with custom rendering and cross-referencing
Built with Verso
The official Lean language reference
The Lean project website
An introduction to using Lean as a proof assistant
Functional Programming in Lean
A hands-on guide to programming in Lean
Terry Tao's Analysis I: a Lean Companion
This page is built in Verso.
Try Verso
Verso lets you write rich, correct, and interactive documents with Lean. Whether you're starting a new textbook, blog, or reference manual, now is a great time to begin.
