ホーム / Technical /

Proving Integer Properties in Lean (1): Introducing Mathlib and Algebraic Structures

Saturday, 15 August 2026

Lean Mathematics Technical

t f B! P L

So far we have proven properties of natural numbers from scratch using MyNat. Starting with this article, we switch to using Mathlib to prove properties of integers. This article covers how to set up Mathlib and the basic algebraic structures we will use in later proofs. Mathlib is a large library of formalized mathematics maintained by the Lean community. The textbook's concept is to build everything from scratch, but from here we change course and use Mathlib to reuse results we have already proven ourselves. This article is based on the book ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.

Setting up Mathlib

Start by importing Mathlib. Add the following to lakefile.lean. 

import Lake
open Lake DSL

package "LearnLean" where
  version := v!"0.1.0"

@[default_target]
lean_lib «LearnLean» where
  globs := #[.submodules `LearnLean]

Running the following commands finishes the setup for using Mathlib. 

$ lake update mathlib
$ lake exe cache get

What is an algebraic structure?

An algebraic structure is a mathematical object obtained by equipping a set with operations. Mathlib provides many algebraic structures out of the box, and by using them we can reuse the proofs we built for natural numbers when working with integers. Below, we look at some of the most basic algebraic structures.

Monoid

For a set X with a binary operation (· * ·): X → X → X, we say X forms a monoid when the following hold.

  • Associativity: ∀ a, b, c ∈ X (a * b) * c = a * (b * c)
  • Existence of an identity: ∃ e ∈ X, ∀ a ∈ X e * a = a = a * e

If in addition the following holds, we call it a commutative monoid.

  • Commutativity: ∀ a, b ∈ X a * b = b * a

Group

For a set X with a binary operation (· * ·): X → X → X, we say X forms a group when the following hold.

  • X is a monoid with respect to (· * ·)
  • Existence of an inverse: ∀ a ∈ X ∃ b a * b = e = b * a, where e ∈ X is the identity

A commutative group is also called an abelian group. A typical example of a commutative group is the set of all integers.

Semiring

For a set X with addition (· + ·) and multiplication (· × ·), we say (X, +, ×) forms a semiring when the following hold.

  • X is a commutative monoid with respect to addition (· + ·), with identity 0
  • X is a monoid with respect to multiplication (· × ·), with identity 1
  • Multiplication distributes over addition: ∀ a b c ∈ X a × (b + c) = a × b + a × c and (a + b) × c = a × c + b × c
  • Multiplying by 0 always gives 0

The set of all natural numbers is a semiring. When multiplication is commutative, it is called a commutative semiring.

Ring

For a set X with addition (· + ·) and multiplication (· × ·), we say (X, +, ×) forms a ring when the following hold.

  • (X, +) is a commutative group
  • (X, +, ×) is a semiring

The set of all integers is a ring. When multiplication is commutative, it is called a commutative ring.

The code is available in the following repository.
https://github.com/ringring-creator/LearnLean

QooQ