Editorial Policy

Purpose

Lean 4 Dev publishes tutorials, references, and course-style lessons for people learning Lean 4. Content is written to help readers understand a concept, run examples, and know where to continue.

Research and sources

Guides are based on hands-on Lean usage, runnable examples, official Lean documentation, Mathlib documentation, and public community resources. External references are linked when they add useful context or provide the canonical source for a tool, tactic, package, or language feature.

Quality standards

• Each page should have a clear learning objective.
• Code examples should be small, focused, and easy to copy into Lean.
• Explanations should add context beyond simply restating documentation.
• Pages should avoid misleading claims, fake scarcity, and placeholder content.

Corrections and updates

Lean and Mathlib evolve. When a reader reports a broken example or outdated step, the issue is reviewed and corrected when reproducible. Priority is given to installation instructions, examples that fail to compile, and explanations that could lead learners in the wrong direction.

Send corrections through the contact page.

Advertising and independence

Advertising may help support hosting and maintenance costs. Ads do not determine tutorial topics, recommendations, or editorial conclusions. The site does not sell positive coverage and does not publish paid tutorials without disclosure.

Authorship

Pages are published under Lean 4 Dev Editorial Team. The site is independent and is not an official Lean FRO publication.