伝統によれば，プログラミング言語は，コンソールに "Hello, world!" と表示するプログラムをコンパイルし，実行することで導入されるべきです．この単純なプログラムは，言語ツールが正しくインストールされ，プログラマがコンパイルされたコードを実行できることを保証します．
しかし，1970年代以降，プログラミングは変わりました．今日，コンパイラは一般的にテキストエディタに統合されており，プログラミング環境はプログラムを書く際にフィードバックを提供してくれます．Lean も例外ではありません：Lean は言語サーバープロトコルの拡張版を実装していて，テキストエディタと通信し，ユーザが入力する際にフィードバックを提供することができます．
Python，Haskell，JavaScript などさまざまな言語が，式やステートメントを入力できる REPL（read-eval-print-loop）を提供しています．REPL は対話的なトップレベル，ブラウザ・コンソールとしても知られています．そしてプログラミング言語はユーザの入力結果を計算し，表示します．一方 Lean は，これらの機能をエディタとのインタラクションに統合し，テキストエディタにプログラムテキスト自体に統合されたフィードバックを表示させるコマンドを提供します．この章では，エディタで Lean を操作する方法を簡単に紹介します．Hello, World！ではバッチモードでコマンドラインから Lean を使用する伝統的な方法を説明します．
この本は，Lean をエディタで開きながら，それぞれの例に沿って入力しながら読むのがベストです．例で遊んで，何が起こるか見てみましょう！