Ricardo's example: specialization raises world output of both goods

Proved

ComparativeAdvantage.ricardo_specialization_gain

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

comparative-advantageeconomicsinternational-trade

In Ricardo's example England has $220$ hours of work and Portugal $170$ . Then

producing one unit each of cloth and wine uses all of England's labour ( $100+120=220$ ) and all of Portugal's ( $90+80=170$ );
if England spends its $220$ hours on cloth it produces $220/100=2.2$ units, and if Portugal spends its $170$ hours on wine it produces $170/80=2.125$ units;
both exceed the $1+1=2$ units of each good produced in autarky.

So, with specialization according to comparative advantage, the global production of both goods increases.

Preamble

import Mathlib
import Definitions.Def_ComparativeAdvantage_Model

Formal statement

namespace ComparativeAdvantage

theorem ricardo_specialization_gain :
    england.aLC * 1 + england.aLW * 1 = england.L ∧
    portugal.aLC * 1 + portugal.aLW * 1 = portugal.L ∧
    england.L / england.aLC = 2.2 ∧ portugal.L / portugal.aLW = 2.125 ∧
    1 + 1 < england.L / england.aLC ∧ 1 + 1 < portugal.L / portugal.aLW := by sorry

end ComparativeAdvantage

Source

Wikipedia, "Comparative advantage" (PDF export supplied with the request); https://en.wikipedia.org/wiki/Comparative_advantage, section "Ricardo's example"

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.

With England $=(L,a_{LC},a_{LW})=(220,100,120)$ and Portugal $=(170,90,80)$ , the statement asserts the conjunction:

$100\cdot1+120\cdot1=220$ ;
$90\cdot1+80\cdot1=170$ ;
$220/100=2.2$ ;
$170/80=2.125$ ;
$1+1<220/100$ ;
$1+1<170/80$ .

There are no variables or hypotheses.

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