Skip to main content
Link
Menu
Expand
(external link)
Document
Search
Copy
Copied
Lean Block Course 2026
Home
Outline
Cheat Sheets
Setup
Quick Reference
Unicode Input
Tactics
Addendum
Prove axiom-free proofs
Naming in case splits
theorem vs lemma
let vs have in tactic mode
When · focusing is optional
VS Code distractions
Proof length
Resources
Search Lean Block Course 2026
GitHub
Cheat Sheets
Quick references for working with Lean 4.
Table of contents
Setup
Quick Reference
Unicode Input
Tactics