Prove2Me

Ricardo's example: Portugal's absolute advantage, England's comparative advantage in cloth

Proved
ComparativeAdvantage.ricardo_advantages

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

comparative-advantageeconomicsinternational-trade

In Ricardo's example England needs 100100 hours of work for one unit of cloth and 120120 for one unit of wine, while Portugal needs 9090 and 8080. Then

  1. Portugal has an absolute advantage in both goods: 90<10090<100 and 80<12080<120;
  2. England has a comparative advantage in cloth:
100120<9080;\frac{100}{120}<\frac{90}{80};
  1. Portugal does not have a comparative advantage in cloth relative to England.
Preamble
import Mathlib
import Definitions.Def_ComparativeAdvantage_Model
Formal statement
namespace ComparativeAdvantage

theorem ricardo_advantages :
    portugal.aLC < england.aLC ∧ portugal.aLW < england.aLW ∧
    HasComparativeAdvantageInCloth england portugal ∧
    ¬ HasComparativeAdvantageInCloth portugal england := 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,aLC,aLW)=(220,100,120)=(L,a_{LC},a_{LW})=(220,100,120) and Portugal =(170,90,80)=(170,90,80), the statement asserts the conjunction:

  1. 90<10090<100;
  2. 80<12080<120;
  3. 100/120<90/80100/120<90/80;
  4. not (90/80<100/12090/80<100/120).

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