LeanBot — Lean and formal verification for economists

Question 1

What exactly is Lean?

A proof begins with definitions and assumptions and argues, step by step, that a conclusion follows. Authors, referees, and readers normally check those steps by hand. Even a careful proof can leave a nagging question: was an assumption used without being stated, was a case missed, or does a step really follow?

is a computer program that checks this logical part of a proof. The definitions, assumptions, conclusion, and proof steps are written in a precise form. Lean checks every step and accepts the proof only if the conclusion follows from the stated definitions and assumptions.

A person or an AI still decides what the symbols mean and writes the formal proof. Lean does not decide whether the assumptions are realistic or whether the formal statement captures the intended economics. It checks whether the reasoning is valid once those choices have been made.

Lean is free to use, and anyone can inspect how it works. Most Lean projects also use Mathlib, a large collection of standard mathematics already checked by Lean. It includes foundations for real numbers, probability, calculus, topology, and linear algebra, so each project does not have to rebuild them from scratch.

Question 2

Can I see a full example?

This is Euclid’s argument that there are infinitely many primes. The theorem says that above every natural-number bound n there is a prime p. Click any line to see exactly what it does.

This exact file was checked with Lean 4 and Mathlib. It contains no unfinished proof and no .

EuclidPrimes.lean

Why this means infinitely many

A finite set of natural numbers has a largest member. Producing a prime above every proposed bound rules out a largest prime.

What Mathlib supplies

The proof imports the existence of a prime divisor and the factorial divisibility lemma. Lean also checks those imported proofs and the earlier proofs on which they depend.

What the says

reports only : propext, Classical.choice, and Quot.sound. There is no .

Economics example

From a model statement to a global optimum

Suppose inverse demand is p(q) = a − bq, cost is cq, b > 0, and c ≤ a. The familiar monopoly quantity (a − c)/(2b) is feasible and maximizes profit among all nonnegative quantities.

Lean makes the demand curve, cost function, feasible domain, and parameter restrictions explicit. It proves global optimality directly; it does not assume that satisfying a first-order condition is sufficient.

What the proof uses

Translation: Profit is written as (a − bq)q − cq, and the proposed quantity is defined exactly. The word is a technical note about exact real-number division, not an economic assumption.
Argument: Lean verifies that the profit gap equals b(q − q*)², which is nonnegative because b > 0.
Boundary: The linear demand and constant-cost model are assumptions; Lean does not decide whether they describe a particular market well.

Checked with Lean 4.33 and Mathlib 4.33. No unfinished proof; the axiom audit reports only standard foundational axioms.

LinearMonopoly.lean

import Mathlib

def monopolyProfit (a b c q : ℝ) : ℝ :=
  (a - b * q) * q - c * q

noncomputable def monopolyQuantity (a b c : ℝ) : ℝ :=
  (a - c) / (2 * b)

theorem linear_monopoly_optimum
    (a b c : ℝ) (hb : 0 < b) (hac : c ≤ a) :
    0 ≤ monopolyQuantity a b c ∧
      ∀ q : ℝ, 0 ≤ q →
        monopolyProfit a b c q ≤
          monopolyProfit a b c (monopolyQuantity a b c) := by
  constructor
  · unfold monopolyQuantity
    positivity
  · intro q _
    have hgap :
        monopolyProfit a b c (monopolyQuantity a b c) -
            monopolyProfit a b c q =
          b * (q - monopolyQuantity a b c) ^ 2 := by
      unfold monopolyProfit monopolyQuantity
      field_simp [ne_of_gt hb]
      ring
    nlinarith [mul_nonneg (le_of_lt hb)
      (sq_nonneg (q - monopolyQuantity a b c))]

#print axioms linear_monopoly_optimum

Question 3

Why is this useful?

Logical confidence

Lean removes the nagging question of whether a formal conclusion actually follows from the assumptions that were stated.

Visible assumptions

Domains, boundary cases, imported results, and hidden dependencies become explicit objects that can be inspected.

Clearer refereeing

Lean can make human referees more confident in your results. If they dispute a statement or step, the formal theorem gives you an objective and precise place to disagree.

Reusable proofs

Once a lemma is formalized, later papers can import it rather than reconstructing the same technical argument.

What does each participant contribute?

Participant	What it does	What it cannot establish alone
LLM	Reads the paper, proposes formal statements, writes Lean, searches for lemmas, and explains errors.	Its output is not a certificate. It can mistranslate the paper or produce code that was never run.
Lean	Mechanically checks that a precise conclusion follows from precise assumptions.	It cannot decide whether the formal statement captures the intended economics.
Computer algebra system	Simplifies expressions, solves equations, differentiates, and checks many calculations.	It generally does not verify the paper’s complete logical argument or the meaning of its assumptions.
Author or referee	Judges the model, assumptions, interpretation, importance, and faithfulness of the translation.	Human review does not mechanically guarantee that every formal step is valid.

Question 4

How does it work?

A formal proof has two boundaries. First, someone must translate the mathematics into an exact statement. Then Lean checks every logical step from that statement to the conclusion.

01

Write the mathematical claim

Definitions, domains, assumptions, and the conclusion are stated without relying on context or notation left elsewhere in the paper.

02

Translate it into Lean

The economic objects become precise mathematical objects, functions, relations, and assumptions. This is the part that requires judgment about meaning.

03

Construct the proof

A person, Lean’s automated tools, or an AI may search for the proof. Imported Mathlib theorems can be used just as a paper uses established mathematics.

04

Let Lean perform the final check

Lean’s small trusted checking program accepts the proof only if it establishes exactly the theorem that was stated.

Semantic check

Does the Lean theorem match the paper’s quantifiers, domains, information, timing, and intended economic meaning? This requires comparison with the source.

Formal check

Given the exact formal statement and its imported dependencies, does the conclusion follow? Lean checks this mechanically.

Question 5

What are the limitations?

Lean checks the formal theorem, not the prose

A perfectly checked proof can still formalize the wrong statement. Quantifiers, domains, timing, information, equilibrium concepts, and strict inequalities must be compared with the paper independently.

The formalization may start partway through the argument

Some formalizations begin from an intermediate equation, lemma, equilibrium characterization, or other result stated in the paper instead of deriving it from the model’s primitive assumptions. Lean then verifies only what follows from that starting point. The report should identify the unproved input and mark the result conditional unless the upstream derivation is also formalized.

Libraries do not contain everything

A standard named mathematical theorem may be absent from Mathlib, or the paper may use an economic object that has not yet been formalized. A report should expose that missing dependency, not hide it behind an axiom without explanation.

Automation still makes semantic mistakes

AI systems can select the wrong theorem, alter an assumption, or prove a convenient special case. Running Lean catches invalid formal reasoning; it does not catch every bad translation or misleading coverage claim.

Empirical work is outside the present scope

LeanBot presently checks mathematical theory, including exact finite calculations and counterexamples. It does not verify data cleaning, estimation, calibration, simulations, or external numerical claims.

Question 6

What exactly was checked in my paper?

Start with , not the Lean source. It maps the paper’s theorem numbers and pages to the corresponding named results in the Lean files, records added assumptions, and identifies where each checked argument begins and ends.

Then compare the in with the literal claim in the paper. That statement—not the theorem’s name or its surrounding commentary—is the exact contract Lean checked.

1

Paper claim

The result as stated in the paper, with its theorem number and page.

2

Formal statement

The exact Lean objects, assumptions, quantifiers, and conclusion.

3

Checked proof

A formal proof that Lean accepts for that exact statement.

Formalization coverage

How much of the paper’s result did Lean check?

Exact

The stated result and the dependency chain represented in the package are proved on the stated domain.

Conditional

The conclusion is proved after one or more upstream results or model equations are taken as explicit inputs.

Narrower

Lean proves a genuine special case, equation, or subresult, but not the complete source claim.

Blocked

No complete proof is claimed. The report identifies the first indispensable missing construction or invalid step.

Finding about the paper

What did the formalization attempt reveal about the source?

No issue found

No logical problem was identified within the portion checked. This does not mean that every result in the paper was formalized.

Clarified

The formalization made an implicit assumption, domain restriction, boundary convention, or definition explicit.

Easily correctable

A small repair makes the result valid without changing its main economic content, and the report states whether the repaired version was checked.

Substantive problem

Recovering the result appears to require a material change to the claim, assumptions, or argument.

These ratings answer different questions. A conditional proof is not evidence of an error, and a fully checked Lean argument can still expose a problem in the paper’s literal statement. Any proposed repair is shown separately from the source claim.

Question 7

Why can I trust the check?

A Lean check has two parts: verifying the formal proof and checking that its formal statement represents the paper. The package and report preserve evidence for both.

Pinned setup

The package records the exact Lean and Mathlib versions used, so the same environment can be reconstructed.

An actual build

The complete project is run through Lean. Code that merely looks plausible is not counted as verified.

No hidden holes

The files are checked for Lean commands that leave a proof unfinished, and every main theorem is checked for unproved assumptions.

Checked dependencies

Imported Mathlib results come with Lean-checked proofs; they are not accepted as informal citations.

A separate translation review

The report compares the formal theorem with the paper and records any changed assumption, restriction, or conditional starting point.

Standard foundational axioms reported by Lean are not hidden economic assumptions. The report distinguishes them from any proposition introduced specifically for the paper.

Question 8

How can I inspect or extend it?

1. Read the package

Begin with REPORT.md. Then inspect the exact theorem statements in Main.lean. The other small project files record which Lean version and mathematical libraries to use, including their exact dependency versions.

2. Ask a coding LLM to run Lean

You do not need to install Lean or type commands yourself. Open the complete folder in a coding LLM that can read files and use a terminal, then paste this prompt:

Open this complete project folder. Do not edit any files yet. Read REPORT.md and use the Lean and Mathlib versions pinned by the project. Install Lean or fetch dependencies if needed, then run the verification command recorded in the report (normally lake exe cache get followed by lake build). Tell me the exact result and every warning. Search for sorry, admit, unsafe, and paper-specific axioms, and run #print axioms for the headline theorems. Do not claim that the package is verified unless Lean actually ran. If verification fails, explain the first error before changing anything.

An ordinary chat without terminal access can explain the code, but it cannot genuinely verify the package.

3. Keep or share it privately

Create a private GitHub repository and add the complete package, not only Main.lean. GitHub Desktop is the easiest route without a command line. Invite coauthors or a referee only when you want them to have access.

Prompts for an AI coding assistant

Give the assistant the paper and the complete package. Use a tool that can inspect files and actually run Lean. Check the provider’s data policy before uploading confidential work.

Explain the package before changing it

Read REPORT.md first, then inspect Main.lean, lean-toolchain, and lakefile.toml or lakefile.lean.

For each headline result, explain:
1. the paper's claim in plain English;
2. the exact Lean theorem statement;
3. every assumption and domain restriction;
4. the main proof structure;
5. important imported theorems; and
6. what remains outside the checked proof.

Do not infer that the translation matches the paper merely because the Lean file compiles. Do not change any files yet.

Compare the formal theorem with the paper

Read the paper and the complete Lean package together.

For every result listed in REPORT.md, make a table with:
- paper theorem or proposition number and page;
- the literal source claim;
- the corresponding Lean declaration;
- differences in quantifiers, domains, strict versus weak inequalities, timing, information, and equilibrium concept;
- assumptions added, removed, or moved upstream; and
- whether the report's coverage label is justified.

Treat compilation and source fidelity as separate questions. Quote only the minimum source text needed to locate each issue. Do not edit the proof.

Continue the formalization without weakening it

Make the smallest honest improvement to this Lean formalization.

Rules:
- do not use sorry, admit, unsafe, or a new axiom;
- do not weaken the conclusion or silently strengthen the assumptions;
- preserve the paper-to-Lean result map;
- if a named mathematical theorem is unavailable, state that dependency explicitly instead of pretending it was proved;
- record any correction to the paper separately from the literal source claim; and
- run the project's documented Lean command after every change.

At the end, show the exact diff, the build result, and #print axioms for every changed headline theorem.

Where can I learn more?

Start here

Lean on Wikipedia

A short independent overview of Lean, its history, and related proof assistants.

Official introduction and FAQ

The Lean project’s own account of its purpose, design, and history; the linked site also contains its FAQ.

A research proof checked in Lean

An accessible Quanta account of the liquid tensor formalization and research-level use of Lean.

Try or learn

Natural Number Game

Try interactive proving in a browser without installing anything.

Mathematics in Lean

A free practical textbook for mathematically mature readers.

Lean community

Discussion forums, meetings, learning materials, and places to ask technical questions.

Technical and research

The Lean 4 system paper

The peer-reviewed technical description of Lean 4 and its proof-checking architecture.

The Mathlib paper

How the shared mathematical library is organized, reviewed, and built for reuse.

Browse Mathlib

Search the definitions and theorems currently available to Lean projects.

Economics projects

Econlib

An emerging Lean library of reusable definitions and results for economic and political theory.

EconCSLib

Formalized game theory, mechanism design, social choice, matching, and related computational economics.

Privacy and disagreement

LeanBot does not publish individual reports, paper titles, author names, or possible mistakes. If you disagree with a report and decide not to change the paper, nothing further is done. The report is for your benefit.

If you disagree, the useful place to begin is the first exact point of divergence: a cited source statement, a theorem signature, an added assumption, or a missing dependency. Reply to the email with the relevant theorem and page.

You do not need to cite, thank, or credit LeanBot. LeanBot is independent and is not affiliated with Lean or any company or institution.