Labs
Exercices pratiques gradés par l'état réel du simulateur — pas par QCM.
Phase 1 — Lean as a language
Polymorphic identityImplement the polymorphic identity function.1/45′Apply twiceImplement a function that applies `f` twice.1/48′Map an optional valueDefine `mapOption` by pattern matching.1/412′Count tree leavesComplete the recursive leaf count.2/420′Create a type class instanceDefine `Named`, then provide an instance for `User`.3/425′
Phase 2 — Proof foundations
Swap a conjunctionProve that conjunction is commutative in one direction.1/410′Chain implicationsCompose two logical implications.1/412′Eliminate a disjunctionUse both branches of a disjunction to derive the same result.2/418′Construct an existential witnessExhibit a natural number equal to `n + n`.1/410′Equality transitivityProve equality transitivity using rewriting or existing equality eliminators.2/415′Map identity over a listProve that mapping the identity function does not change a list.2/425′Length of appendProve that length turns append into addition.2/430′Associativity of appendProve append associativity without using the library theorem.3/435′
Phase 3 — Mathlib and proof engineering
Set inclusion transitivityProve transitivity of subset inclusion elementwise.2/415′Intersection commutativityProve set intersection commutativity using extensionality.2/420′Polynomial normalizationProve the difference-of-squares identity over integers.2/410′Antisymmetry by linear arithmeticDerive equality from two opposite inequalities over rationals.2/410′Enumerate a small naturalUse Presburger arithmetic to enumerate naturals below three.2/410′Divisibility transitivity by witnessesProve divisibility transitivity by unpacking witnesses.3/425′Linear map extensionalityProve two linear maps equal from pointwise equality.3/420′Continuity of compositionUse the library API to prove composition preserves continuity.3/415′