Approved Lean libraries

Choose a fixed profile when posting a problem. These libraries are hosted by hunch; checking runs on a separate verifier origin in a WebAssembly worker, without access to your account or local files.

This catalogue covers the supported modules, not every module in Mathlib. External packages and build scripts are not accepted. Download the catalogue.

Lean core

Profile: core

Exact imports and example proof

import Init

∀ n : Nat, n + 0 = n

by
  intro n
  rfl

Mathlib (browser subset)

Profile: mathlib

Exact imports and example proof

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

∀ x : ℝ, (x + 1) ^ 2 = x ^ 2 + 2 * x + 1

by
  intro x
  ring

Standard library — lists, arrays, maps

Profile: std

Exact imports and example proof

import Std
import Batteries
import Lean.Elab.Tactic.Omega

∀ xs : List Nat, xs.reverse.reverse = xs

by
  intro xs
  simp

Finite sets and counting

Profile: discrete

Exact imports and example proof

import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Tactic.NormNum

∀ s t : Finset Nat, (s ∪ t).card ≤ s.card + t.card

by
  intro s t
  exact Finset.card_union_le s t

Number theory — primes and divisibility

Profile: number_theory

Exact imports and example proof

import Mathlib.Data.Nat.Prime.Infinite
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Int.ModEq
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring

∀ p : Nat, Nat.Prime p → 2 ≤ p

by
  intro p hp
  exact hp.two_le

Algebra — groups, rings, polynomials

Profile: algebra

Exact imports and example proof

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Eval.Defs
import Mathlib.GroupTheory.QuotientGroup.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum

∀ p : Polynomial ℝ, p + 0 = p

by
  intro p
  simp

Linear algebra — matrices and linear maps

Profile: linear_algebra

Exact imports and example proof

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Mul
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

∀ A : Matrix (Fin 2) (Fin 2) ℝ, A * 1 = A

by
  intro A
  simp

Topology — continuity, limits, metric spaces

Profile: topology

Exact imports and example proof

import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Topology.Algebra.Order.Field
import Mathlib.Topology.Instances.RealVectorSpace
import Mathlib.Tactic.Linarith

∀ f g : ℝ → ℝ, Continuous f → Continuous g → Continuous (fun x => f x + g x)

by
  intro f g hf hg
  exact hf.add hg

Real analysis — sequences, exp, log, trigonometry

Profile: analysis

Exact imports and example proof

import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

∀ x : ℝ, Real.exp x > 0

by
  intro x
  exact Real.exp_pos x

Graph theory — paths, cycles, colouring

Profile: graph_theory

Exact imports and example proof

import Mathlib.Combinatorics.SimpleGraph.Paths
import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.Tactic.NormNum

∀ (G : SimpleGraph (Fin 3)) (u v : Fin 3), G.Adj u v → G.Adj v u

by
  intro G u v h
  exact h.symm

Computability — Turing machines and undecidability

Profile: computability

Exact imports and example proof

import Mathlib.Computability.TuringMachine.StackTuringMachine
import Mathlib.Computability.Halting

∀ n : Nat, ¬ ComputablePred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c n).Dom)

by
  intro n
  exact ComputablePred.halting_problem n

Probability — distributions, independence, expectations

Profile: probability

Exact imports and example proof

import Mathlib.Probability.ProbabilityMassFunction.Basic
import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Probability.Independence.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Tactic.NormNum

∀ p : PMF Bool, ∑' b : Bool, p b = 1

by
  intro p
  exact p.tsum_coe

Calculus — derivatives, extrema, convex optimisation

Profile: calculus

Exact imports and example proof

import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.LocalExtr.Basic
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

∀ x : ℝ, HasDerivAt id 1 x

by
  intro x
  exact hasDerivAt_id x