Mathematics in Lean

Build the essential foundations for writing and reading proofs in Lean, progressing from propositions and proof terms to logical connectives, quantification, equality, and basic tactic use.

• ·Course Introduction

  Welcome and orientation to Mathematics in Lean. Learn how the course progresses from foundational logic through mathematical structures, induction, analysis, and integrated theorem proving.

• ·Propositions

  Learn how Lean represents statements that can be proved or disproved. Examine proposition syntax and recognize the role of propositions in theorem declarations.

• ·Propositions as Types

  Develop the propositions-as-types perspective underlying Lean's logic. Read proof terms as inhabitants of proposition types and interpret theorem declarations through this correspondence.

• ·Implication

  Study implication as a function from proofs of one proposition to proofs of another. Practice introducing an assumption and using it to derive a conclusion.

• ·Conjunction

  Learn how the logical connective And packages proofs of two propositions. Use its introduction and elimination principles to build and extract conjunctive proofs.

• ·Disjunction

  Study the logical connective Or and its alternatives. Learn how to prove a selected branch and reason by considering the possible branches of an existing disjunction.

• ·Universal Quantification

  Learn how Forall expresses a proposition for every value of a type. Practice introducing an arbitrary value and applying a universally quantified hypothesis to a specific value.

• ·Equality

  Study equality as an inductive proposition with reflexivity as its fundamental proof. Learn to use equality hypotheses for substitution and to recognize definitional equality.

• ·Basic Tactic Proofs

  Learn the basic tactic commands that expose the structure of a goal and its hypotheses. Use these tactics to carry out direct proof construction without obscuring the underlying logical principles.

• Foundational Proof Synthesis

  Demonstrate foundational proof fluency by reading theorem types, selecting appropriate introduction and elimination principles, and expressing the resulting reasoning with Lean tactics.

Extend foundational proposition and proof skills with negation, equivalence, existential reasoning, quantifier transformations, and classical proof principles in Lean.

• ·False

  False is the proposition with no constructors or proofs. Learners examine how a proof of False can produce a proof of any proposition through false elimination.

• ·Negation

  Negation is represented as an implication from a proposition to False. Learners construct negations and apply them to assumptions to derive contradictions.

• ·Biconditional

  A biconditional states that two propositions imply one another. Learners prove each direction separately and use the resulting equivalence in both directions.

• ·Existential Quantification

  An existential proposition asserts that some witness satisfies a property. Learners provide witnesses when constructing existential proofs and extract witnesses and their properties when analyzing them.

• ·Unique Existence

  Unique existence combines the existence of a witness with a proof that every qualifying witness equals it. Learners work with the logical structure of Lean's unique-existence proposition.

• ·Quantifier Negation

  Negated quantifiers relate statements such as not every object satisfying a property and the existence of an object that does not satisfy it. Learners distinguish constructive directions from equivalences that require classical reasoning.

• ·Contraposition

  Contraposition transforms an implication from P to Q into an implication from not Q to not P. Learners construct this reasoning explicitly using assumptions and contradiction.

• ·Law of Excluded Middle

  The law of excluded middle states that every proposition is either true or false. Learners use Lean's classical reasoning tools to perform a complete case split on an arbitrary proposition.

• ·Proof by Contradiction

  Proof by contradiction reduces the goal P to showing that not P is impossible. Learners identify the contradiction-producing assumptions and connect the method to classical reasoning.

• Logical Structure Synthesis

  This synthesis assessment requires learners to select and coordinate appropriate logical forms and proof strategies. Problems integrate constructive reasoning with classical case analysis while preserving the structure of the propositions involved.

Develop the ability to express and prove algebraic facts in Lean across common algebraic structures, using normalization and arithmetic automation to reason about numerical, polynomial, linear, and nonlinear relationships.

• ·Algebraic Expressions

  Learn how Lean represents algebraic expressions involving numerals, addition, multiplication, powers, subtraction, and division, and how type inference determines their meaning.

• ·Semirings

  Understand the operations and laws provided by Lean's semiring hierarchy, including additive and multiplicative identities, associativity, commutativity, and distributivity.

• ·Rings

  Extend semiring reasoning to rings, where every element has an additive inverse and subtraction is available. Learn how ring assumptions support general algebraic identities.

• ·Fields

  Understand how fields extend rings with inverses for nonzero elements, and how Lean represents division and the conditions required for manipulating denominators.

• ·Numerical Normalization

  Use `norm_num` to evaluate numerical expressions and discharge straightforward arithmetic goals while respecting the ambient algebraic type.

• ·Ring Normalization

  Learn how ring normalization expands, rearranges, and canonicalizes polynomial expressions so that algebraic identities can be proved without manually managing individual rearrangement steps.

• ·Linear Arithmetic

  Use linear arithmetic reasoning to combine hypotheses involving variables with constant coefficients and establish equalities or inequalities in ordered algebraic structures.

• ·Nonlinear Arithmetic

  Extend arithmetic automation to nonlinear polynomial relationships, using `nlinarith` to derive consequences from hypotheses involving products, squares, and higher powers.

• Algebraic Reasoning Synthesis

  Synthesize algebraic expression analysis, structural assumptions, numerical and ring normalization, and linear or nonlinear arithmetic to construct reliable Lean proofs of varied algebraic claims.

Learn how inductive types and propositions support mathematical reasoning in Lean, then use ordinary and strong induction together with recursive definitions to prove properties of natural numbers and lists.

• ·Inductive Types

  Inductive types are defined by specifying their constructors, which describe how their elements are formed. Learners examine how Lean represents and analyzes values of inductive types.

• ·Inductive Propositions

  Inductive propositions describe evidence by listing the constructors that generate valid proofs. Learners use these constructors to build proofs and understand what cases an inductive proposition permits.

• ·Natural Number Induction

  Natural number induction reduces a statement about every natural number to a base case and a step from an arbitrary number to its successor. Learners connect this mathematical principle to the inductive structure of `Nat`.

• ·Induction Tactic

  The `induction` tactic applies an inductive type's recursor and creates goals for its constructors. Learners identify the generated cases and use the induction hypotheses in the appropriate goals.

• ·Structural Recursion

  Structural recursion defines a function by analyzing an inductive argument and making recursive calls only on structurally smaller parts. This pattern mirrors the constructors of the underlying inductive type.

• ·Recursive Definitions

  Recursive definitions specify the result for each constructor case and may call themselves on smaller inputs. Learners use pattern matching and recursive equations to express computations over inductive data.

• ·List Induction

  List induction follows the two constructors of lists: the empty list and adding an element to an existing list. Learners use the induction hypothesis to reason about the tail in the cons case.

• ·Generalizing Induction Hypotheses

  An induction hypothesis can become too specific when variables are fixed before the induction variable. Learners recognize this situation and use generalization to obtain a hypothesis that applies in the inductive step.

• ·Strong Induction

  Strong induction permits the inductive step to use the proposition for every predecessor below the current number, rather than only the immediately preceding number. Learners express this principle with Lean's natural-number induction tools.

• Induction and Recursion Synthesis

  Learners analyze the inductive structure of a statement or data type, select an appropriate induction principle, and reason about recursive definitions and their equations. The assessment requires coordinating induction hypotheses, constructor cases, and termination-aware recursive reasoning.

Learn how Lean represents mathematical structures and manages relationships between types through structures, typeclasses, subtypes, coercions, equivalence relations, and quotient types.

• ·Structures

  Structures package several fields into a single type, allowing mathematical objects and their associated data to be represented together. Learners examine structure declarations, field types, and structure values.

• ·Structure Projections

  Every structure field generates a projection that extracts the corresponding component from a structure value. Learners use projections explicitly and understand how Lean infers their structure argument.

• ·Structure Extensionality

  Structure extensionality reduces equality between structured objects to equality of their fields. Learners apply extensionality principles and the `ext` tactic to organize these proofs.

• ·Typeclasses

  Typeclasses are structures whose instances describe capabilities or laws associated with a type. Learners formulate polymorphic definitions and theorems that use typeclass parameters.

• ·Instance Synthesis

  Lean uses instance synthesis to find values for implicit typeclass arguments. Learners trace available instances, diagnose failed synthesis, and provide explicit instances when inference needs help.

• ·Subtypes

  A subtype packages an element with a proof that it satisfies a predicate. Learners construct subtype terms, access their values and proofs, and state propositions about restricted collections of objects.

• ·Coercions

  Coercions insert type conversions automatically when Lean expects an underlying value, such as using a subtype element where its ambient type is required. Learners distinguish convenient coercion from explicit conversion.

• ·Equivalence Relations

  Equivalence relations formalize when elements should be regarded as representing the same object. Learners package the three defining properties and use them to reason about equivalence classes.

• ·Quotient Types

  Quotient types identify elements related by an equivalence relation and support reasoning about equivalence classes rather than representatives. Learners use quotient lifts and soundness conditions to define operations and establish quotient properties.

• Advanced Structures Synthesis

  This synthesis assessment evaluates the ability to select appropriate representations and reason across Lean's advanced mechanisms for organizing mathematical objects. Learners connect structured data, inferred algebraic capabilities, restricted types, and quotient reasoning in a coherent formal proof.

Combine Lean definitions, theorem statements, library exploration, rewriting, simplification, calculation chains, local lemmas, and goal inspection into a disciplined workflow for developing readable and reliable mathematical proofs.

• ·Definitional Abstraction

  A Lean definition gives a reusable name to a type, term, or mathematical construction. Learners examine how definitions support abstraction while remaining available for unfolding when needed.

• ·Theorem Statements

  A theorem statement specifies the exact proposition that a proof must establish. Learners practice choosing quantified variables, typeclass assumptions, and hypotheses that faithfully represent mathematical claims.

• ·Library Search

  Lean's libraries provide definitions, lemmas, and theorems that prevent redundant proof work. Learners use declaration inspection and search tools such as `#check`, `#find`, and documentation lookup to identify relevant results.

• ·Rewriting

  Rewriting replaces an expression with an equal or logically equivalent expression. Learners control the direction and location of rewrites so that existing lemmas expose a more useful proof state.

• ·Simplification

  The simplifier repeatedly applies trusted simplification rules, definitions, and hypotheses to normalize common logical and algebraic forms. Learners distinguish automatic simplification from directed rewriting and supply additional lemmas when necessary.

• ·Calculation Chains

  A `calc` block presents a chain of intermediate expressions, recording the theorem that justifies each transition. Learners use calculation chains to make transitive reasoning explicit and readable.

• ·Local Lemmas

  Local lemmas divide a proof into named intermediate claims that can be reused in the remaining goal. Learners formulate these claims at the right level of generality and prove them from the current context.

• ·Goal Inspection

  Effective formalization depends on understanding the exact state Lean is checking at each step. Learners inspect local contexts and targets to diagnose mismatched terms, missing assumptions, and unsuitable tactic choices.

• ·Proof Refactoring

  Proof refactoring improves structure without changing the proposition being proved. Learners compare alternative proof steps and organize a proof so that its mathematical dependencies and transformations are explicit.

• Integrated Formalization Synthesis

  This capstone assesses an integrated formalization workflow from mathematical interpretation through proof completion and refactoring. Learners must explain why each definition, theorem, and proof step fits the evolving Lean goal.