入力法は、コマンド "lean4: Show all abbribiations" で表示される。
| 文字 | 名前 | 番号 | 入力法 | 用途 |
| “λ” | Greek Small Letter Lamda | U+03BB | \lam | ラムダ抽象 |
| “↦” | Rightwards Arrow from Bar | U+21A6 | \map | ラムダ抽象の区切り |
| “·” | Middle Dot | U+00B7 | \. | 無名ラムダ変数 |
| “∘” | Ring Operator | U+2218 | \o | 反図式順結合 |
| “≫” | Much Greater-Than | U+226B | \gg | 図式順結合（圏論） |
| “∣” | Divides | U+2223 | \| | 算術述語「割り切れる」 |
| “⊢” | Right Tack | U+22A2 | \ent | ゴールの区切り |
| “↑” | Upwards Arrow | U+2191 | \upar | コアージョン |
| “✝” | Latin Cross | U+271D | 不明 | アンカリー化された変数 |
| “▸” | Black Right-Pointing Small Triangle | U+25b8 | 不明 | イコールのリカーサー |
