Game theory, economics, finance, and other social and behavioral sciences
The Lean Pool projects whose card's first MSC2020 code is in class 91, “Game theory, economics, finance, and other social and behavioral sciences”: 5 articles, one per card.
TheoremApportionmentlib#
Formalizes apportionment rules and proves the Balinski-Young impossibility theorem: no anonymous quota rule can be population-monotone.
Quoted from the card LeanPool/projects/apportionment.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Apportionment.balinski_young(theorem; a main declaration), declared in LeanPool/Apportionment/Basic.lean, line 221: “Proves that no anonymous quota apportionment rule can satisfy population monotonicity.”
Project
- Authors: Michał Dobranowski.
- Source: https://archive.org/details/fairrepresentati00bali.
- Project repository: mdbrnowski/apportionmentlib.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 91B12, 91B14.
- In Lean Pool: LeanPool/Apportionment, from the card LeanPool/projects/apportionment.yaml.
Sources
TheoremExistence of Nash equilibria via Brouwer's fixed-point theorem#
Formalizes Scarf's combinatorial lemma, derives Brouwer's fixed-point theorem on a simplex and on finite products of simplices, and uses it to prove the existence of a mixed Nash equilibrium in every finite game.
Quoted from the card LeanPool/projects/brouwer.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ExistsNashEq(theorem; a main declaration), declared in LeanPool/Brouwer/Nash.lean, line 497: “Every finite game has a mixed Nash equilibrium.” Its source, as the card gives it: “J. Nash, Equilibrium Points in N-Person Games, Proceedings of the National Academy of Sciences 36(1):48-49, 1950, doi:10.1073/pnas.36.1.48.”Brouwer(theorem; a main declaration), declared in LeanPool/Brouwer/Brouwer.lean, line 729: “Every continuous self-map of a standard simplex has a fixed point.” Its source, as the card gives it: “H. Scarf, The Approximation of Fixed Points of a Continuous Mapping, SIAM Journal on Applied Mathematics 15(5):1328-1343, 1967, doi:10.1137/0115116.”Brouwer_Product(theorem; a main declaration), declared in LeanPool/Brouwer/BrouwerProduct.lean, line 610: “Every continuous self-map of a finite product of simplices has a fixed point.” Its source, as the card gives it: “H. Scarf, The Approximation of Fixed Points of a Continuous Mapping, SIAM Journal on Applied Mathematics 15(5):1328-1343, 1967, doi:10.1137/0115116.”IndexedLOrder.Scarf(theorem; a main declaration), declared in LeanPool/Brouwer/Scarf.lean, line 1864: “Scarf's combinatorial lemma producing a colorful simplex.” Its source, as the card gives it: “H. Scarf, The Approximation of Fixed Points of a Continuous Mapping, SIAM Journal on Applied Mathematics 15(5):1328-1343, 1967, doi:10.1137/0115116.”FinGame(structure; a main declaration), declared in LeanPool/Brouwer/Nash.lean, line 75: “The structure of a finite game with finitely many players and finite pure strategy sets.” Its source, as the card gives it: “J. Nash, Equilibrium Points in N-Person Games, Proceedings of the National Academy of Sciences 36(1):48-49, 1950, doi:10.1073/pnas.36.1.48.”FinGame.mixedNashEquilibrium(def), declared in LeanPool/Brouwer/Nash.lean, line 171: “The predicate that a mixed strategy profile is a Nash equilibrium.” Its source, as the card gives it: “J. Nash, Equilibrium Points in N-Person Games, Proceedings of the National Academy of Sciences 36(1):48-49, 1950, doi:10.1073/pnas.36.1.48.”
Project
- Authors: Math_XMUM.
- Source: doi:10.1073/pnas.36.1.48.
- Project repository: math-xmum/Brouwer.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2025 Math_XMUM”.
- MSC2020: 91A06, 91A10, 47H10.
- In Lean Pool: LeanPool/Brouwer, from the card LeanPool/projects/brouwer.yaml.
Sources
TheoremMisere combinatorial games#
Formalizes a combinatorial game theory library for misere play, including comparison modulo universes, p-free forms, outcome-stability, Property X, and concrete rulesets such as Hackenbush.
Quoted from the card LeanPool/projects/misere-games.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
MisereGames.Form.Promain.of_universe(theorem; a main declaration), declared in LeanPool/MisereGames/Misere/Comparison.lean, line 572: “Shows that comparison modulo a universe is characterized by the maintenance-proviso test.”MisereGames.IntegerInvertible.isPFree_of_propertyX(theorem), declared in LeanPool/MisereGames/Misere/OutcomeStable/PropertyX.lean, line 599: “Proves that Property X makes the sum of two short p-free games p-free in an outcome-stable, hereditary, integer-invertible monoid.”MisereGames.Form.Preservation.endLikeSeedToUniverse_bijective, which the scan does not find declared in the project's files at this commit: “Proves that universal closure gives a bijection from bounded end-like seeds to universes.”
Project
- Authors: Tomasz Maciosowski, Alfie Davies.
- Source: misere-games by Tomasz Maciosowski, Alfie Davies, Violeta Hernandez Palacios, Yuyang Zhao.
- Project repository: t4ccer/misere-games.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 91A46, 05C57.
- In Lean Pool: LeanPool/MisereGames, from the card LeanPool/projects/misere-games.yaml.
Sources
TheoremNormalized capped log-household clearing and dynamic programming#
Proves conditional uniqueness of a rate solving the unit-wage normalized clearing equation: mean household assets equal α / ((1 - α) * (r + δ)), with α = 9/25 and δ = 2/25. Households have capped log utility, discount 24/25, no borrowing, and monotone finite earnings transitions with positive one-step access to a lowest-income state; an explicit cap-slack inequality is required. Finite Tauchen chains instantiate the household model. Bisection converges to a given solution of this normalized equation along a stationary-distribution selection. Equivalence to full competitive market clearing for arbitrary earnings scales is not established. Preserves Bellman contraction, Berge maximum theorems, stationary Markov theory, Euler inequalities, consumption concavity and marginal-propensity bounds.
Quoted from the card LeanPool/projects/aiyagari-equilibrium.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanEconomics.aiyagariTauchen_equilibriumRate_unique_Ioo(theorem; a main declaration), declared in LeanPool/AiyagariEquilibrium/Models/AiyagariTauchenWitness.lean, line 112: “For capped log households with discount 24/25, no borrowing and a finite Tauchen chain with persistence in [0,1), two rates in (-2/25, 1/24) whose stationary household distributions have mean assets equal to 9 / (16 * (r + 2/25)) coincide, provided the explicit asset-cap inequality holds at their larger rate. This is the prescribed unit-wage normalized clearing equation; a bridge to full competitive equilibrium for arbitrary earnings scales is not supplied.”LeanEconomics.IncomeFluctuation.aiyagari1994_log_bisection(theorem), declared in LeanPool/AiyagariEquilibrium/Equilibrium/Bisection.lean, line 231: “Given a rate satisfying the same unit-wage normalized clearing equation in a compact interval inside (-2/25, 1/24), a stationary-distribution selection and the stated cap, monotonicity and reachability hypotheses, bisection on normalized excess supply brackets that rate, bounds midpoint error by the initial width divided by 2^(n+1), and has left endpoints converging to it. Existence of a solution to this equation is assumed.”LeanEconomics.continuousAt_maxValue(theorem), declared in LeanPool/AiyagariEquilibrium/Topology/Berge.lean, line 142: “A continuous objective maximized over a nonempty compact-valued correspondence that is upper and lower hemicontinuous has a continuous maximum value at the parameter.”LeanEconomics.Blackwell.contractingWith(theorem), declared in LeanPool/AiyagariEquilibrium/DynamicProgramming/Blackwell.lean, line 116: “A monotone operator on bounded continuous real functions that discounts constants by a nonnegative factor below one is a contraction with that factor.”
Project
- Authors: Robert Kirkby.
- Project repository: LeanEconomics/LeanEconomics, at commit 8295256b.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 91B50, 90C39, 60J05.
- In Lean Pool: LeanPool/AiyagariEquilibrium, from the card LeanPool/projects/aiyagari-equilibrium.yaml.
Sources
TheoremScott's measurement representation theorems#
Formalizes all eight numbered finite representation theorems of Dana Scott's 1964 Measurement Structures and Linear Inequalities. Develops a shared finite separation and rational-cancellation engine, unit-threshold semiorder representations, additive utility on pairs, ordered utility differences, and normalized finitely additive probabilities on finite Boolean algebras. Includes the Kraft-Pratt-Seidenberg five-atom counterexample to de Finetti's weaker axioms and local real embeddings of finite subsets of ordered abelian groups. A separately labelled modern infinite analogue assumes a generalized Kelley condition: strict-comparison vectors have a countable cover by closed convex upper sets avoiding zero above the weak-comparison cone. It is neither a countably additive measure theorem nor an attribution of Scott's unpublished infinite theorem. The infinite construction uses universal probability evaluation vectors, with a proved faithful Stone representation and probability-state correspondence. The upstream proofs were produced primarily by AI agents under Lars Warren Ericson's direction and review.
Quoted from the card LeanPool/projects/scott-measurement.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 12 main results, each with its informal statement quoted from the card. The scan finds 12 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_1(theorem), declared in LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean, line 223: “For a finite symmetric subset X of a finite-dimensional real normed space, membership in an arbitrary set N on X is represented by nonnegativity of a linear functional if and only if every x in X has x or -x in N and every zero sum of positively real-weighted vectors from X intersect N has all their negatives in N.”Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_2(theorem), declared in LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean, line 261: “For a finite symmetric set of rational-valued vectors on a finite coordinate type, the same linear realizability criterion uses unweighted zero sums, with repetitions allowed, instead of arbitrary positive real weights.”Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_3(theorem), declared in LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean, line 328: “A relation on a finite set of rational-valued vectors on a finite coordinate type is represented exactly by comparison of one real linear functional if and only if it is complete and, whenever two equally indexed finite lists have equal sums and every left vector is related to its right partner, all the reverse comparisons also hold.”Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_4(theorem), declared in LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean, line 403: “A relation on a finite rational vector set is represented by one real linear functional if and only if it extends to its zero-inclusive additive submonoid closure as a complete relation preserving addition and satisfying Scott's cancellation axiom.”Scott1964.MeasurementStructures.theorem_2_1(theorem), declared in LeanPool/ScottMeasurement/Preference/Intransitive.lean, line 91: “On any finite set (allowing the empty case, unlike the source), a relation P admits real scores with P x y exactly when the score of x is at least the score of y plus one if and only if P is irreflexive and satisfies Scott's two four-alternative semiorder axioms.”Scott1964.MeasurementStructures.theorem_3_1(theorem), declared in LeanPool/ScottMeasurement/Differences/Pair.lean, line 187: “On the product of any two finite sets (also allowing empty coordinate types), a relation admits an additive representation f(x)+g(x') exactly when it is total and satisfies Scott's cancellation scheme for independent permutations of the two coordinates.”Scott1964.MeasurementStructures.theorem_3_2(theorem), declared in LeanPool/ScottMeasurement/Differences/Ordered.lean, line 105: “On any finite set (also allowing the empty case), a quaternary relation D is represented exactly by comparisons f(x)-f(y) >= f(z)-f(w) for one real utility f if and only if D is total and satisfies permutation cancellation and reversal.”Scott1964.MeasurementStructures.theorem_4_1_vector(theorem; a main declaration), declared in LeanPool/ScottMeasurement/Probability/Finite.lean, line 484: “A relation on a finite Boolean algebra is represented exactly by a nonnegative normalized finitely additive real probability if and only if the certain event is strictly above null, every event is at least null, comparisons are total, and Scott's cancellation scheme holds whenever two finite lists have equal sums of atom characteristic vectors.”Scott1964.MeasurementStructures.LinearInequalities.finite_local_real_embedding(theorem), declared in LeanPool/ScottMeasurement/LinearInequalities/OrderedGroup.lean, line 198: “Every finite subset of a linearly ordered abelian group has a real-valued map reflecting its order and preserving every addition equation whose three terms lie in the subset; this asserts a local map, not an embedding of the entire group.”Scott1964.MeasurementStructures.Probability.KPSCounterexample.deFinetti_axioms_insufficient(theorem), declared in LeanPool/ScottMeasurement/Probability/KPSCounterexample.lean, line 254: “The explicit Kraft-Pratt-Seidenberg order on the 32 events of five atoms satisfies de Finetti's five qualitative-probability axioms but has no normalized finitely additive real probability representing all comparisons.”Scott1964.MeasurementStructures.Probability.Infinite.reconstructed_infinite_theorem_4_1(theorem), declared in LeanPool/ScottMeasurement/Probability/Infinite/Reconstructed.lean, line 220: “On an arbitrary Boolean algebra, a relation admits an exact normalized finitely additive real probability representation if and only if it is nontrivial, nonnegative relative to null, total, and satisfies the stated generalized Kelley cover condition on its universal event-span comparison vectors. This is a modern analogue with an explicit extra analytic condition.”Scott1964.MeasurementStructures.Probability.Infinite.probabilityStateEquiv(def), declared in LeanPool/ScottMeasurement/Probability/Infinite/EventSpace.lean, line 387: “Finitely additive probabilities on an arbitrary Boolean algebra are canonically equivalent to positive normalized continuous linear functionals on the real span of its universal probability-evaluation vectors, equipped with the inherited supremum norm.”
Project
- Authors: Lars Warren Ericson.
- Source: Measurement Structures and Linear Inequalities by Dana Scott, Journal of Mathematical Psychology 1 (1964), 233-247.
- Project repository: catskillsresearch/scott1964, at commit 591e8a6a.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 91B16, 91B06, 60A05, 52A20.
- In Lean Pool: LeanPool/ScottMeasurement, from the card LeanPool/projects/scott-measurement.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.