AGENTS.md - Guide for Theorem Proving and Lean 4 in This Repository

This file provides guidance for AI agents working on theorem proving in Lean 4 within this repository.

How to Run Things

There are three main ways to interact with Lean 4 code in this project:

1. Pipe Code Directly into the Lean Compiler

You can test arbitrary Lean 4 expressions by piping them directly to the compiler:

echo 'def foo := "bar"' | lake env lean --stdin

Important: The current working directory must be the project root for this to work properly.

2. Build Individual Files

To compile a specific file, for example located at ./Lib/Problem.lean, use :

lake env lean ./Lib/Problem.lean

3. Build the Entire Project

To build all files in the project:

lake build

Note: This project will have many files that compile with “sorries.” That is ok. In general, you will be asked to provide a valid proof for a single Problem. When you are done, that file should compile without sorries.

It is not likely that you need to compile the whole project, but the option is there if you find that you need it.

How to Explore Mathlib

Location of Mathlib

The source code to Mathlib is located in .lake/packages/mathlib/. This directory is the root of the Mathlib project, and .lake/packages/mathlib/Mathlib contains the source code to the library.

Searching for Theorems and Definitions

The easiest way to find relevant theorems and lemmas is to use your search tools (like rg or Grep) to search through mathlib:

# Search for theorems about modular arithmetic
rg "theorem.*mod" --type lean .lake/packages/mathlib/Mathlib/Data/ZMod/

# Search for specific function names
rg "pow_card" .lake/packages/mathlib/Mathlib/

Useful Tactics

ring: Solves equality goals in rings using normalization
simp: Simplifies expressions using the simp lemma database
rw: Rewrite using specific lemmas
calc: Chain equalities/inequalities step by step (very useful for modular arithmetic!)
exact: Provide the exact proof term
contradiction: Derive a contradiction from contradictory hypotheses

Style Guide

Theorem Documentation

Every theorem must have a doc comment (/-- ... -/) above it with a natural language statement:

/--
For any prime p and any natural number a not divisible by p,
a raised to the power (p-1) is congruent to 1 modulo p.
-/
theorem fermat_little_theorem (p : ℕ) (a : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) :
    a ^ (p - 1) ≡ 1 [MOD p] := by
  ...

Proof Structure

Proofs should be well-structured using have clauses to break down the argument into logical steps. Each have clause should:

Have a natural language comment above it explaining the step
Contain a short proof (ideally 2-3 lines of tactics)
Represent a step that a mathematician would make (possibly implicitly)

Example:

theorem fermat_little_theorem (p : ℕ) (a : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) :
    a ^ (p - 1) ≡ 1 [MOD p] := by
  -- We need the fact that p is prime as a typeclass instance
  haveI : Fact p.Prime := ⟨hp⟩

  -- p is positive since it is prime
  have hp_pos : 0 < p :=
    hp.pos

  -- a is nonzero in ZMod p since p does not divide a
  have ha_nonzero : (a : ZMod p) ≠ 0 := by
    intro h
    rw [ZMod.natCast_eq_zero_iff] at h
    contradiction

  ...

Using Calc Mode

For proofs involving chains of equalities or inequalities, you can use calc mode:

-- Therefore, a^(p-1) * a = a in ZMod p
have pow_pred_times_a : (a : ZMod p) ^ (p - 1) * (a : ZMod p) = (a : ZMod p) := by
  calc (a : ZMod p) ^ (p - 1) * (a : ZMod p)
      = (a : ZMod p) ^ (p - 1 + 1) := by rw [pow_succ]
    _ = (a : ZMod p) ^ p := by rw [Nat.sub_add_cancel hp_pos]
    _ = (a : ZMod p) := pow_card

Nested Have Clauses vs. Lemmas

You can nest have clauses within other have clauses, similar to inner functions in Python. However, if you find yourself creating deep trees of nested have clauses, consider extracting independent lemmas instead:

-- Sometimes useful to keep as nested have clauses (doesn't clutter namespace)
have outer : ... := by
  have inner1 : ... := ...
  have inner2 : ... := ...
  ...

-- But if the structure gets complex, extract to a lemma
lemma helper_result : ... := by
  ...

theorem main_theorem : ... := by
  have step1 := helper_result
  ...

Complete Example: Fermat’s Little Theorem

Here’s a complete example demonstrating all the style guidelines:

import Mathlib

namespace FermatLittle

open Nat ZMod

/-
# Fermat's Little Theorem

This file contains a proof of Fermat's Little Theorem, which is fundamental
in number theory and modular arithmetic.
-/

/--
For any prime p and any natural number a not divisible by p,
a raised to the power (p-1) is congruent to 1 modulo p.
-/
theorem fermat_little_theorem (p : ℕ) (a : ℕ) (hp : p.Prime) (ha : ¬ p ∣ a) :
    a ^ (p - 1) ≡ 1 [MOD p] := by
  -- We need the fact that p is prime as a typeclass instance
  haveI : Fact p.Prime := ⟨hp⟩

  -- p is positive since it is prime
  have hp_pos : 0 < p :=
    hp.pos

  -- a is nonzero in ZMod p since p does not divide a
  have ha_nonzero : (a : ZMod p) ≠ 0 := by
    intro h
    rw [ZMod.natCast_eq_zero_iff] at h
    contradiction

  -- In a finite field, every element raised to the cardinality equals itself
  have pow_card : (a : ZMod p) ^ p = (a : ZMod p) :=
    ZMod.pow_card (a : ZMod p)

  -- Therefore, a^(p-1) * a = a in ZMod p
  have pow_pred_times_a : (a : ZMod p) ^ (p - 1) * (a : ZMod p) = (a : ZMod p) := by
    calc (a : ZMod p) ^ (p - 1) * (a : ZMod p)
        = (a : ZMod p) ^ (p - 1 + 1) := by rw [pow_succ]
      _ = (a : ZMod p) ^ p := by rw [Nat.sub_add_cancel hp_pos]
      _ = (a : ZMod p) := pow_card

  -- Canceling a from both sides (valid since a ≠ 0), we get a^(p-1) = 1
  have pow_eq_one : (a : ZMod p) ^ (p - 1) = 1 := by
    calc (a : ZMod p) ^ (p - 1)
        = (a : ZMod p) ^ (p - 1) * 1 := by ring
      _ = (a : ZMod p) ^ (p - 1) * ((a : ZMod p) * (a : ZMod p)⁻¹) := by
          rw [← mul_inv_cancel₀ ha_nonzero]
      _ = ((a : ZMod p) ^ (p - 1) * (a : ZMod p)) * (a : ZMod p)⁻¹ := by ring
      _ = (a : ZMod p) * (a : ZMod p)⁻¹ := by rw [pow_pred_times_a]
      _ = 1 := mul_inv_cancel₀ ha_nonzero

  -- Converting from ZMod p equality to natural number congruence
  rw [← ZMod.natCast_eq_natCast_iff]
  simp only [Nat.cast_pow, Nat.cast_one]
  exact pow_eq_one

end FermatLitte

Breaking Down the Example

Searching for Premises: The key theorems used are:
- ZMod.pow_card: Found by searching for “pow” and “card” in mathlib
- ZMod.natCast_eq_natCast_iff: Found by searching for conversion between ZMod and Nat
- mul_inv_cancel₀: Standard group theory lemma
Have Clause Structure: Each have clause has:
- A clear natural language comment
- A short proof (often just one or two tactics)
- A logical step in the overall argument
Calc Mode Proofs: Used twice to show chains of equalities clearly
Natural Language Comments: Every major step is documented so a mathematician can follow the proof without reading tactics

This style makes proofs readable, maintainable, and educational!