Formalized textbooks:
Dynamic Programming: Sargent & Stachurski (Vol 1 & 2); Stokey, Lucas & Prescott
Monetary: Gali (NK); Woodford (interest & prices); Cochrane (fiscal theory).
International: Obstfeld & Rogoff
500+ corrections (mostly tiny or typo)
github.com/LeanEconomics
Dynamic Programming: Sargent & Stachurski (Vol 1 & 2); Stokey, Lucas & Prescott
Monetary: Gali (NK); Woodford (interest & prices); Cochrane (fiscal theory).
International: Obstfeld & Rogoff
500+ corrections (mostly tiny or typo)
github.com/LeanEconomics
github.com LeanEconomics Formalizing Economics in Lean. LeanEconomics has 6 repositories available. Follow their code on GitHub.