Formalising “100” Theorems/Models/Theories in Economics

This page attempts to do for theorems in economics what Freek Wiedijk’s page does for mathematical theorems more generally. It inherits the same caveats, as well as adopting a dynamic definition of 100.

To date, 7 of the 54 listed theorems have been formalized.

Theorems in the list which have not been formalized yet are in italics.

1. Abreu-Pearce-Stachetti

2. Afriat’s theorem

3. Arrow's impossibility theorem

   • Isabelle (Gammie)

   • Isabelle (Nipkow)

   • Mizar (Wiedijk)

   • (Tang and Lin)

4. Aumann's theorem on rationality

   • Coq (Vestergaard, Lescanne and Ono)

5. Bayes' theorem

6. Black-Scholes Formula

7. Bondareva–Shapley theorem

8. Central limit theorems

9. Coase theorem

10. Core convergence theorem

11. Crawford-Sobel informative cheap talk

12. Debreu’s open gap theorem

13. Diamond-Mirrlees efficiency theorem

14. Duggan–Schwartz theorem

15. Envelope theorem

16. Factor price equalization theorem

17. Fisher separation theorem

18. Folk theorem

19. Frisch–Waugh–Lovell theorem

20. Fundamental theorems of asset pricing

21. Gale’s deferred acceptance [algorithm]

22. Gauss–Markov theorem

23. Gibbard–Satterthwaite

    • Isabelle (Nipkow)

24. Girsanov theorem

25. Glivenko-Cantelli theorem

26. GMM: consistent, asymptotically normal and efficient

27. Greenwald-Stiglitz theorem

28. Heckscher–Ohlin theorem

29. Holmström's theorem

30. Kuhn’s theorem

    • Coq (Vestergaard)

31. Minimax theorem

32. MLE: consistent, asymptotically normal, asymptotically efficient, invariant

33. May's theorem

    • Isabelle (Gammie)

34. Muller-Satterthwaite

    • (Tang and Lin)

35. Modigliani–Miller capital structure irrelevance

36. Nash's bargaining solution

37. Nash's existence theorem

38. Negishi’s theorem

39. No trade theorem

40. Purification theorem

41. Revelation principle

42. Rybczynski theorem

43. Sen's Paretian liberal

    • Isabelle (Gammie)

    • (Tang and Lin)

44. Sklar's theorem

45. Slutsky's identity

46. Sonnenschein–Mantel–Debreu theorem

47. Stolper–Samuelson

48. Tobin–Markowitz two-fund separation theorem

49. Topkis' theorem

50. von Neumann–Morgenstern utility representation theorem

51. Welfare economics: first fundamental theorem

52. Welfare economics: second fundamental theorem

53. Wold's representation theorem

54. Zermelo's theorem