Verso — Written in Lean, checked by Lean

Verso

Verso

Written in Lean. Checked by Lean.

Verso is a platform for writing documents, books, course materials, and websites with Lean.<br>Every code example is type-checked. Every rendered page is interactive. And it's all<br>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:<br>```lean<br>def Set (α : Type u) : Type u :=<br>α → Prop

instance : Membership α (Set α) where<br>mem xs x := xs x<br>```<br>A function $`f` is surjective if each element of the range is covered by an element of the domain:<br>```lean<br>def Surjective (f : α → β) :=<br>∀ y, ∃ x, f x = y<br>```<br>:::theorem "Cantor"<br>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:<br>```lean<br>theorem cantor (f : S → Set S) : ¬ Surjective f := by<br>intro h<br>have ⟨x, p⟩ := h (fun x : S => x ∉ f x)<br>have : x ∈ f x ↔ x ∉ f x := by<br>constructor<br>simp [Membership.mem] at *<br>grind<br>grind<br>```<br>:::

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 :=<br>α → Prop

instance : Membership α (Set α) where<br>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 : α → β) :=<br>∀ y, ∃ x, f x = y

Cantor

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 := byS:Type u_1f:S → Set S⊢ ¬Surjective f<br>intro hS:Type u_1f:S → Set Sh:Surjective f⊢ False<br>have ⟨x, p⟩ := h (fun x : S => x ∉ f x)S:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ False<br>have : x ∈ f x ↔ x ∉ f x := byS:Type u_1f:S → Set S⊢ ¬Surjective f<br>constructormpS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ x ∈ f x → ¬x ∈ f xmprS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ ¬x ∈ f x → x ∈ f x mpS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ x ∈ f x → ¬x ∈ f xmprS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬x ∈ f x⊢ ¬x ∈ f x → x ∈ f x<br>simp [Membership.mem] at *mprS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x x → f x x mpS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x xmprS:Type u_1f:S → Set Sh:Surjective fx:Sp:f x = fun x => ¬f x x⊢ ¬f x x → f x x<br>grindAll goals completed! 🐙<br>grindAll 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.<br>Different kinds of documents are called genres.<br>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

Lean Reference Manual

The official Lean language reference

lean-lang.org

The Lean project website

Theorem Proving in Lean 4

An introduction to using Lean as a proof assistant

Functional Programming in Lean

A hands-on guide to programming in Lean

Analysis I

Terry Tao's Analysis I: a Lean Companion

This Very Page

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...