- Author
- Not stated (published on the overreacted blog)
- Published
- 2 September 2025
- Kind
- Personal blog tutorial with code examples
- Original
- overreacted.io/a-lean-syntax-primer/
- Subject
- Checkable specs for coding agents
- Themes
- Saying it exactly, Getting good
What it is
The overreacted blog published this primer. The page names no author. It calls itself opinionated and incomplete, and warns of possible inaccuracies. The writer says the writer is still learning Lean.
What it says
- A Lean file can run code, prove facts about code, or do both.
- A theorem about a function is like a test, but for all possible inputs.
- Tactics such as unfold, decide and omega transform a goal until it is closed.
- Lean calls take no parentheses or commas: write f a b c.
- Implicit and instance arguments are filled in by Lean, and the at-sign shows them.
- The closing example interleaves a list append function with proofs about its length.
What evidence it gives
The primer offers worked code throughout. Each step is shown in the Lean editor with the goal state. One example shows a proof failing after the formula changes. There is no benchmark or survey.
Interests and limits
This is one person's teaching approach, by its own account. The examples are deliberately contrived, such as ages and birth years. The primer covers syntax, not large verified systems. Its claim about Lean use in industry is one brief sentence.