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.

AI mathematics and proof stories

Proof Stories is a dated, curated collection. We distinguish a new proof, a counterexample, a partial result, a formalization of existing mathematics, and a competition result. A company announcement is attributed to the company; a released Lean artifact does not automatically establish independent review, correct interpretation of the formal statement, or prize recognition.

Each story links original research, the available formalization, and specific X posts. When direct X access is unavailable, we record that limitation and use primary mathematical sources for the result itself. We do not invent tweet quotations, engagement counts, or controversies. Disputes are presented with attributed accounts and responses.

“Sources checked” means the linked documents were reviewed. It does not mean we compiled a large Lean project. Code excerpts are labeled as statements, excerpts, or examples; they are never presented as a complete proof when they are not one.

Forum discussions

Forum contributions are public, user-submitted discussion, not editorial endorsement. Guest names are unverified. Discuss mathematical claims constructively, cite evidence, credit contributors, and do not post private information or impersonate others. Authors can remove their own posts using the browser that created them. Report concerns with the report control; moderators can hide posts and lock discussions.

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.