Terms of Use

Last updated: September 14, 2026

Educational content

Lean 4 Dev publishes educational content about Lean 4 programming and theorem proving. The material is provided for learning and reference. It is not a substitute for official Lean documentation, professional software review, or academic advice.

Academy purchases and compiler use

The pricing page states the content, price and compiler credits included with each purchase. The Academy Pass is a one-time purchase that gives the purchasing account permanent access to the paid course edition and hides advertising. It does not renew. A compiler-credit pack is also a one-time purchase; unused purchased credits do not expire.

A compiler check is one submitted run, including a run that finds an error in the code. Every account also receives a monthly free allowance, which resets at the start of each calendar month in UTC. Purchased credits are used only after that allowance. A compiler or network failure does not consume a check.

The playground is for small educational programs and proofs. It is not a persistent server or a general hosting service. Do not attempt to evade usage limits, access another user’s data, or interfere with the service. A successful compilation with an unfinished proof warning does not establish that the proof is complete.

Use the electronic withdrawal and refund function for an eligible recent purchase, or contact [email protected] for a billing error or another statutory claim. These terms do not restrict consumer rights that apply by law. A preview explicitly labeled Stripe test mode does not accept real payments.

Acceptable use

• Use the site for learning, teaching, and research.
• Do not attempt to disrupt, scrape abusively, or attack the site.
• Do not submit malicious code, spam, or private credentials through contact channels.

Accuracy

Lean and Mathlib change over time. The site aims to keep examples useful, but code snippets may need adjustment for future Lean or Mathlib versions. Corrections can be sent through the contact page.

Intellectual property

The Lean name, Lean project, and Mathlib belong to their respective communities and rights holders. Lean 4 Dev is independent and is not officially affiliated with the Lean FRO.

Code examples on the site are intended for learning and adaptation unless a specific page states otherwise.

Advertising

Free access may include Google advertising. Academy Pass holders receive an ad-free site experience after their account status has loaded in the browser. Advertising does not influence lessons, references, or editorial decisions.

Availability and corrections

We maintain the course, account service, and hosted compiler with reasonable care. Temporary maintenance, provider outages, or safety limits may interrupt compiler access. Purchased credits remain on the account during an interruption. Report incorrect lessons or unavailable paid access to [email protected].

Contact

Questions about these terms can be sent to [email protected].

See also the Privacy Policy, Legal Notice, and Editorial Policy.