Prove2Me

Say's identity: aggregate value of demand equals aggregate value of supply

Proved
SaysLaw.aggregate_supply_eq_aggregate_demand

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

economicsgeneral-equilibriummacroeconomicssays-law

Throughout, ι\iota is a finite set of agents and GG a finite set of goods; p=(pg)g∈Gp=(p_g)_{g\in G} is a real price vector; si=(si,g)gs_i=(s_{i,g})_g and di=(di,g)gd_i=(d_{i,g})_g are real vectors giving the quantities agent ii brings to market (supplies) and plans to buy (demands); ⟨p,x⟩=∑g∈Gpgxg\langle p,x\rangle=\sum_{g\in G}p_g x_g is the market value of a bundle xx; and zg=∑i∈ι(di,g−si,g)z_g=\sum_{i\in\iota}(d_{i,g}-s_{i,g}) is the aggregate excess demand for good gg.

Suppose every agent obeys Say's budget principle at prices pp: ⟨p,di⟩=⟨p,si⟩\langle p,d_i\rangle=\langle p,s_i\rangle for all ii. Then the total value of planned purchases equals the total value of goods offered for sale:

∑i∈ι⟨p,di⟩=∑i∈ι⟨p,si⟩.\sum_{i\in\iota}\langle p,d_i\rangle=\sum_{i\in\iota}\langle p,s_i\rangle .

This is the aggregate form of Say's law in the article: the goods offered for sale are evidence of an equal quantity of demand.

Preamble
import Mathlib
import Definitions.Def_SaysLaw_Model
Formal statement
namespace SaysLaw

theorem aggregate_supply_eq_aggregate_demand {ι G : Type*} [Fintype ι] [Fintype G]
    (p : G → ℝ) (supply demand : ι → G → ℝ) (hsay : SaysBudget p supply demand) :
    ∑ i, bundleValue p (demand i) = ∑ i, bundleValue p (supply i) := by sorry

end SaysLaw
Source
Wikipedia, "Say's law" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Say%27s_law
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, with full knowledge of the source article and of the intended meaning. It is not independent, blind testimony and must not be mistaken for one. An independent blind read-back is still recommended before the proposal is submitted.

Let ι\iota (agents) and GG (goods) be arbitrary finite types, possibly empty. Let p:G→Rp:G\to\mathbb R be any real price vector (no sign condition) and let s,d:ι→G→Rs,d:\iota\to G\to\mathbb R be arbitrary real arrays. Assume that for every i∈ιi\in\iota,

∑g∈Gpg di,g=∑g∈Gpg si,g.\sum_{g\in G}p_g\,d_{i,g}=\sum_{g\in G}p_g\,s_{i,g}.

Then

∑i∈ι∑g∈Gpg di,g=∑i∈ι∑g∈Gpg si,g.\sum_{i\in\iota}\sum_{g\in G}p_g\,d_{i,g}=\sum_{i\in\iota}\sum_{g\in G}p_g\,s_{i,g}.

When ι\iota is empty both sides are 00. The statement is a plain equality of real numbers; nothing is asserted about individual goods.

Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph