Intelligence in common.
Who benefits?
AI, work and democratic commons: a founding text, explicit institutional models and conditional proofs you can inspect.
When production depends less on work
If AI can sustain production and innovation with less human labor, income from work may cease to give everyone access to what society produces. The decisive question becomes who owns the infrastructure, who receives its output, and who sets its priorities.
A sufficiently productive common infrastructure could support universal access and democratic economic choices. Its feasibility is an explicit hypothesis, not a consequence of the current capabilities of AI.
Essential provision, with an optional stronger criterion
The foundational commitments are equal liberties and effective democracy (J1), and universal essential provision whenever it is feasible (J3). The earlier maximin criterion (J2) remains available as an optional strengthening, with all its existing results.
Lean proves that maximin implies the sufficiency commitment and that the converse fails. These moral commitments are declared choices. Formal verification checks their consequences, not their moral authority.
Work, property and freedom in an AI society
This text sets out the position being explored. The correspondence below distinguishes its philosophical framing, institutional requirements and conditional mathematical results.
See how each argument is represented
The shared vocabulary
- cᵢ(r), bᵢ
- Actual access under regime r and positive essential needs of person i, measured in the same resource units.
- Q(r)
- The minimum of cᵢ(r)/bᵢ across people. The Lean model requires a person attaining it; Q ≥ 1 means that every essential need is covered.
- Y, λ, θᵢ, τ
- Net consumable output, labor share, private capital-income share, and the fraction of capital income shared equally.
- cᵢ
- ℓᵢ + (1 − τ)θᵢΠ + τΠ/n ; Π = (1 − λ)Y
Loading the theory…
From premises to consequences
More output. For whom?
Start with output of 100, a labor share of 80% and no redistribution. Change the automated economy below. The third column shares collective output equally. Owners are the same people in both private scenarios.
| Group | Before automation | Automated private regime | Collective allocation |
|---|
The initial 90-person loss example and the exact redistribution calculation are checked in Lean. Slider scenarios are browser calculations illustrating the model; they are not economic forecasts or fresh Lean proofs.
What the formalization establishes
Lean checks conditional deductions over exact rational quantities. It does not prove that automation eliminates work, that a majority will lose, or that communism is uniquely superior. Collective ownership, mixed systems and broad private ownership must be compared through their actual feasibility, needs coverage and democratic guarantees.
All displayed theorem statements and proofs are synchronized with the Lean source and compiled by continuous integration. The browser displays precompiled proofs; it does not run Lean. No result is admitted and no philosophical premise is declared as a global Lean axiom.