Dark Forest Theory: A Formal Derivation黑暗森林理论：一个形式化推导

0. Introduction

The “Dark Forest Theory” proposed by Liu Cixin in the Three-Body Problem series is a speculative theory about interaction strategies among cosmic civilizations. This article reconstructs it formally, with tools from game theory and decision theory, starting from the axioms given in the novel ¹.

The argument proceeds in four steps. First, we show that the novel’s two axioms are insufficient on their own to derive the Dark Forest. Then we add the structural conditions the novel relies on and build an incomplete-information game. From it we derive when the Dark Forest’s two behaviors, silence and preemption, are equilibria. Finally we check the theory’s evolutionary claim with a simulation, and discuss the limits of the conclusion. The formal claims are checked in Lean 4 with Mathlib; the proof file is attached as DarkForest.lean, and each checked claim below names its theorem. Section 8.7 says what the proofs cannot settle and what they leave out. Section 9 tests the evolutionary clause in a richer model by simulation. The same proofs, with a project that builds and checks them, are at github.com/changkun/dark-forest-lean.

The short version: the two halves of the Dark Forest are not equally strong. Silence follows under weak conditions. Preemption after detection is only one of two equilibria, and it is the safer one only when strikes usually succeed.

1. Axiomatic System

Let $\mathcal{U}$ be the set of all civilizations in the universe, with $|\mathcal{U}| \geq 2$.

Axiom A1 (Survival Axiom): In the novel, “survival is the primary need of civilization.” For any civilization $c_i \in \mathcal{U}$ and any two outcomes $o, o'$: if $c_i$ survives in $o$ and not in $o'$, then $c_i$ strictly prefers $o$, whatever else differs between them. Writing $S_i(o)$ for “$c_i$ survives in $o$":

$$S_i(o) \wedge \neg S_i(o') ;\Longrightarrow; o \succ_i o'$$

Survival has lexicographic priority. Because survival takes only two values, this order can be represented by a real-valued utility (Lean: lex_representable), unlike the lexicographic order on pairs of real numbers, which has none (lex_real_not_representable). The additive form used below, $-M$ for extinction plus the other gains, represents it exactly when those gains are bounded and $M$ exceeds twice their bound (additive_lex_of_bounded); if the other gains could grow without bound, no finite $M$ would do (additive_not_lex_of_unbounded). The model below assumes bounded gains and a very large $M$.

Axiom A2 (Growth and Finite Resources): In the novel, “civilization continuously grows and expands, but the total matter in the universe remains constant.” Let $R$ be the total resource quantity of the universe and $r_i(t)$ the resources held by civilization $c_i$ at time $t$. Each civilization tends to grow, while

$$\sum_{i} r_i(t) \leq R, \quad \forall t$$

so one civilization’s expansion eventually compresses the resources available to others.

2. Insufficiency of the Axioms

Before proceeding to the formal derivation, it is necessary to address a fundamental question: can the Dark Forest be derived from A1 and A2 alone?

Proposition 0: A1 and A2 alone cannot imply the Dark Forest.

Proof (by counterexample construction): Let two civilizations $c_1, c_2$ satisfy A1 (survival priority) and A2 (finite resources). Consider scenarios in which any of the following additional conditions hold:

(a) Verifiable intentions: There exists a mechanism enabling $c_1$ to reliably verify $c_2$’s goodwill, and vice versa. In this case, both parties can confirm the other’s non-hostility, and cooperation becomes a sustainable equilibrium. In the model of Section 5, a verified strike probability of zero makes waiting strictly better than striking (Lean: prop0_verified), and with no hostile share left, being detected costs nothing, so revealing beats hiding (prop0_verified_reveal).

(b) Enforceable contracts: There exists an enforceable interstellar treaty mechanism (e.g., arbitration by a super-civilization or some universe-level locking protocol), such that violators are punished. Cooperation can then be maintained by institutional means. If the mechanism destroys a violator with probability at least $q^2$, waiting is strictly better than striking whatever the other side does, since the attacker then risks at least as much as waiting ever can (Lean: prop0_enforced).

(c) Defense significantly dominates offense: If technological conditions make first strikes nearly impossible to succeed (defense costs are far lower than offense costs), then a surprise attack has no positive expected payoff, and the security dilemma does not escalate. In the model of Section 5, a strike that never succeeds is strictly worse than waiting whenever it costs anything (Lean: prop0_no_preemption_when_strikes_fail).

(d) Minimal communication delay with frequent interaction: If civilizations can interact at high frequency, then by the Folk Theorem, patient participants can sustain cooperative equilibria in repeated games ². Lean checks the simplest form of this: if the other side answers any strike by striking in every later round, restraint is a best reply exactly when the discount factor per round is at least $(g-w)/(g-p)$. Here $w$, $g$ and $p$ are the per-round payoffs of mutual restraint, of striking a restrained other, and of mutual striking, with $p < w < g$, and being struck while restraining pays no more than $p$ (grim_sustains). With a round-trip delay $\tau$ and a discount rate $r$, the condition reads $r\tau \le \log\frac{g-p}{g-w}$ (grim_delay), the product that condition B3 below turns on. The same holds in any finite game, for any finite number of players: if a pure profile pays everyone more than some stage Nash equilibrium, reverting to that equilibrium after any departure sustains the profile as a subgame-perfect equilibrium once players are patient enough (folk_nash_reversion, folk_subgame_perfect, folk_patient). This is Friedman’s folk theorem, and the two-action game above is a case of it (twoAction_folk).

Under any of these conditions, even with finite resources and survival priority, both parties may maintain peace through division of labor, trade, boundary agreements, or deterrence equilibria.

Therefore, A1 and A2 at most imply that “conflict pressure exists” or “a security dilemma may arise,” but they cannot imply “one must remain silent and destroy upon discovery.” $\square$

Implication: The Dark Forest is not a direct logical consequence of the two axioms. To complete the derivation, additional conditions regarding information structure, communication constraints, and capability evolution must be supplied.

3. Structural Conditions

The following five conditions, together with A1 and A2, form a sufficient set of assumptions for the Dark Forest. Two of them formalize concepts the novel itself introduces alongside its axioms: the chain of suspicion (B2) and the technological explosion (B4) ¹. Each is used: dropping any one alone admits a case in which a conclusion of the Dark Forest fails, as the cases of Proposition 0 show (Lean: each_condition_used). Whether the informal conditions are logically independent of one another is not a question a formal model can settle.

Condition B1 (Anarchic Structure): There exists no supra-sovereign institution in the universe capable of enforcing adjudication, punishing contract violations, or imposing peace. Formally, there is no external enforcement function $E$ such that any agreement $A_{ij}$ between civilizations can be credibly enforced.

Condition B2 (Unverifiable Intentions): For any two civilizations $c_i, c_j$, $c_i$ cannot reliably infer the true type $\theta_j \in {\text{benign}, \text{hostile}, \text{neutral}}$ of $c_j$. Let $m_j$ be any signal emitted by $c_j$. Then:

$$P(\theta_j \mid m_j) = P(\theta_j), \quad \forall m_j$$

Communication is cheap talk and carries no verifiable information about intentions. Benign and hostile civilizations can emit identical signals.

Condition B3 (Light-Speed Lag): Information propagation speed is bounded (at most the speed of light $c$). Let $d_{ij}$ be the distance between civilizations $c_i$ and $c_j$. The minimum round-trip communication delay is $\tau_{ij} \geq 2d_{ij}/c$. This implies:

• Verification cycles are extremely long: any information about the other party’s current state is already outdated.
• Repeated game frequency is extremely low: the Folk Theorem requires sufficiently high interaction frequency and sufficiently low discount rates. When $\tau_{ij}$ is very large, the effective discount factor $\delta \approx e^{-r\tau_{ij}} \to 0$, making the Folk Theorem’s cooperation conditions hard to satisfy. What matters is the product $r\tau_{ij}$: a civilization with a long enough horizon (small $r$) partly escapes this argument.
• This is a physical constraint, independent of civilizations' willingness or technological level.

Condition B4 (Technological Explosion): A civilization’s technological capability may undergo exponential growth in a time span far shorter than a communication cycle. Let $x_i(t)$ be the strategic capability of civilization $c_i$ at time $t$, with evolution:

$$x_i(t + \tau) = x_i(t) \cdot e^{g_i \tau + \xi_i}$$

where $g_i$ is the base growth rate and $\xi_i$ is a random term with positive variance $\sigma^2 > 0$. If the random term can take arbitrarily large values, as a Gaussian one does, a current $x_j(t) \ll x_i(t)$ does not bound $x_j(t + \tau)$: any level, however high, is reached with positive probability (Lean: explosion_possible). Positive variance alone does not give this: a bounded random term, however variable, never lifts a capability that starts far enough below a level to reach it (explosion_needs_reach).

Condition B5 (First-Mover Advantage): Once both parties have located each other, a first strike can, under certain parameter conditions, significantly increase the attacker’s survival probability. Let $q$ be the probability that a strike succeeds and $K_i$ the cost of striking. There exists a non-empty parameter interval in which the expected utility of a first strike exceeds that of restraint.

4. Formal Model

4.1 Utility Function

Let the extinction loss be $M$ (taken to be extremely large), the first-strike cost be $K_i$, and the ordinary gains from cooperation/trade be $G_i$. The utility of civilization $c_i$ is:

$$U_i = -M \cdot \mathbf{1}{\text{extinction}} - K_i \cdot \mathbf{1}{\text{first strike}} + \varepsilon G_i$$

where $M \gg K_i \gg \varepsilon G_i$. This structure reflects A1: survival overrides everything, and no cooperation gain, however large, outweighs “not being annihilated.” With bounded gains, a finite $M$ larger than twice their bound represents A1’s order exactly, as shown above; where a conclusion relies on “$M$ large”, the propositions below say how large.

4.2 Threat Probability

Define the following probabilities:

• $p$: prior probability that the other party is currently hostile
• $\gamma$: probability that the other party, currently non-hostile, evolves into a lethal threat within the verification window $\tau$ (driven by B4)
• Base threat probability: $\pi = 1 - (1-p)(1-\gamma)$

$\pi$ integrates two types of risk: the other party is dangerous now, or the other party is not dangerous now but will become so soon. By B4, with a random term that can be arbitrarily large, $\gamma > 0$ (explosion_possible); by B2 (unverifiable intentions), $p$ cannot be updated to 0. Therefore $\pi > 0$ (Lean: basePi_pos), even if no civilization is hostile now.

In the game after exposure, what matters is the probability that the other side strikes regardless of what we do, and we use $\pi$ for it. Counting $\gamma$ into that probability assumes that a civilization which becomes able to destroy another also becomes willing to. This is part of how we read B4, not a consequence of it.

5. Core Derivation

Proposition 1: Peace Declarations Cannot Constitute Credible Commitments

By B2, signals carry no verifiable information. Any “I have no hostile intent” declaration is cheap talk: benign and hostile civilizations alike can emit identical signals.

Therefore, for any peace declaration $m$, $P(\text{the other is a threat} \mid m) = \pi$ (Lean: prop1_posterior_is_prior), and as long as $0 < \pi < 1$ (prop1_cheap_talk):

$$0 < P(\text{the other is a threat} \mid m) < 1$$

Communication cannot eliminate fear. Not because no one would express goodwill, but because hostile parties would express goodwill too.

Proposition 2: The Chain of Suspicion Unravels Only When Fear Exceeds the Threshold for Striking

Under the constraints of B2 and B3, $c_i$ faces not only first-order uncertainty about “whether the other is dangerous,” but also recursive higher-order uncertainty:

• Order 0: The other party may be a threat, with probability $\pi$
• Order 1: Even if the other party is not a base threat, it may preemptively strike out of fear of me
• Order 2: Even if the other party does not fear me, it may fear that I fear it…

A tempting shortcut is to set the probability of “striking out of fear” equal to the current threat estimate $r_n$, which gives the recurrence

$$r_0 = \pi, \qquad r_{n+1} = \pi + (1 - \pi) r_n$$

with solution $r_n = 1 - (1-\pi)^{n+1}$, which tends to 1 for every $\pi > 0$ (Lean: linearChain_closed, linearChain_tendsto_one). The algebra is right, but the shortcut carries the conclusion. Write $F(r)$ for the share of non-hostile civilizations that would strike if they believed the other side strikes with probability $r$; $F$ is the distribution function of their action thresholds. The chain of suspicion is then

$$r_0 = \pi, \qquad r_{n+1} = \pi + (1 - \pi) F(r_n)$$

The shortcut is the special case $F(r) = r$, in which action thresholds are spread uniformly over $[0, 1]$ (linear_is_uniform). Nothing in A1, A2 or B1–B5 says they are spread that way. Proposition 3 below says what a threshold is: a civilization strikes when $r$ exceeds $r^\ast \approx 1 - q$. If civilizations are alike, $F$ is a step at $r^\ast$, and the chain either stops at once or collapses at once:

• if $\pi \le r^\ast$, then $r_n = \pi$ for every $n$: no civilization that is not already a threat ever strikes (chain_stops);
• if $\pi > r^\ast$, then $r_n = 1$ from the first step on (chain_unravels).

In general, the chain never passes a resting point: any $\bar r \ge \pi$ with $\pi + (1-\pi)F(\bar r) \le \bar r$ bounds it for ever (chain_le_resting_point), so it reaches certainty only if no resting point lies below 1 (chain_below_one_of_resting_point). The chain of suspicion therefore does not by itself carry fear to certainty. It does so only when the base threat already exceeds the threshold for striking, or when thresholds are spread so that no resting point remains. Figure 1 lets you move $\pi$, the typical strike success $q$ and the spread of thresholds, and watch where the chain stops.

Proposition 3: After Exposure, Striking and Restraint Are Both Equilibria

Once both parties have located each other, civilization $c_i$ chooses between striking first and waiting. Let $q$ be the probability that a strike succeeds, the same for both sides, and $r$ the probability that the other side strikes. Being struck kills with probability $q$; a strike that fails reveals the attacker, and the target’s return strike kills with probability $q$. The expected utilities of waiting ($W$) and attacking ($A$) are:

$$U_i(W) = -r q M, \qquad U_i(A) = -(1 - q) q M - K_i$$

For $q > 0$, striking first beats waiting if and only if

$$r > r^\ast = 1 - q + \frac{K_i}{qM}$$

(Lean: prop3_threshold). As $M$ grows, the threshold falls to $1 - q$, and no further (threshold_tendsto). A large extinction loss makes a civilization strike at any fear above $1 - q$; it does not make it strike at any fear at all.

The game after exposure is therefore a stag hunt. Suppose a share $\pi$ of civilizations strikes regardless, and non-hostile ones strike with probability $a$, so that the other side strikes with probability $\pi + (1-\pi)a$:

• Mutual striking ($a = 1$) is an equilibrium whenever $r^\ast < 1$ (strike_equilibrium_iff), that is, whenever $K_i < q^2 M$ (threshold_lt_one_iff).
• Mutual restraint ($a = 0$) is an equilibrium exactly when $\pi \le r^\ast$ (wait_equilibrium_iff): the same condition under which the chain of suspicion stops.
• Striking is risk-dominant ³, the better reply to an even chance of either, exactly when $r^\ast < (1+\pi)/2$ (strike_risk_dominant_iff); for large $M$ this reads $q > (1-\pi)/2$ (strike_risk_dominant_iff_q).

Restraint is the better equilibrium for both sides, since both survive; striking is the safer bet when strikes usually succeed. When each side observes the payoffs with a little noise, players of two-by-two games like this one coordinate on the risk-dominant equilibrium ⁴. Lean checks this for the game here. Let each civilization see only a noisy signal of $q$, that is, $q$ plus a noise of mean zero, drawn independently from a law with no atoms, and start from the textbook case of a flat prior over $q$. Then in every equilibrium, symmetric or not, both sides strike when their signal exceeds $(1-\pi)/2$, the boundary of risk dominance, and wait when it falls below; the threshold strategy is itself an equilibrium (global_game_pair, global_game_unique, threshold_is_equilibrium, selected_is_risk_dominant). The noise enters through one property: a civilization whose signal sits exactly at the threshold gives even odds that the other side’s signal is higher, since of two independent, identically distributed noises that do not tie, each is as likely to be the larger (noise_half, flatNoise). A flat prior over the whole line is not a proper distribution, so Lean also treats a uniform prior on an interval, and there it derives the beliefs instead of assuming them: a signal away from the interval’s ends carries no information about the noises, so the belief about the other side’s signal and the expected value of $q$ are exactly the flat prior’s (interior_signal, belief_is_conditional, posterior_mean). For such noise bounded by $\sigma$, selection then holds at every noise level, not only in the limit, once the prior extends at least $2\sigma$ into each region where one action is better whatever the other side does; in the payoff normalized for large $M$, these are $q < 0$ and $q > 1-\pi$ (uniform_prior_selects). For other priors Lean proves a bound: if beliefs stay within $\eta$ of the uniform prior’s, every equilibrium switches within $(2-\pi)\eta$ of $(1-\pi)/2$ (global_game). For a prior whose range reaches into both dominance regions, and whose density there is at least $m$ and changes by at most $L$ per unit of $q$, Bayes' rule keeps beliefs within $\eta = \max(\sigma, 2L\sigma/(m-L\sigma))$ (conditional_of_density, smooth_prior_selects). The band therefore closes on $(1-\pi)/2$ as the noise shrinks, whatever the noise’s law (smooth_prior_limit). This is the step of Carlsson and van Damme’s argument that the game here needs. Under each of these priors, and whatever the beliefs near its edges, an equilibrium exists (equilibrium_exists), so none of these statements is about an empty set. Lean also proves the result beyond this game, for every two-by-two coordination game in which the state shifts a side’s gain from acting by the same amount whatever the other does. Under a flat prior with the same payoffs on both sides, every equilibrium switches exactly at the risk-dominance boundary, at every noise level (cvd_symmetric, cvd_risk_dominant). With different payoffs and noise bounded by $\sigma$, both sides switch within $2\sigma$ of the point where their indifference probabilities sum to one, provided that point lies outside both sides' dominance regions, and exactly there as the noise vanishes (cvd_asymmetric_flat, cvd_asymmetric_limit); that point is the risk-dominance boundary of Harsanyi and Selten for asymmetric games (cvd_theta_is_risk_dominance). So the post-exposure logic of the Dark Forest holds, but for a narrower reason than an unbounded chain of suspicion: when $q > (1-\pi)/2$, preemption is the safer answer to not knowing what the other side will do. When strikes usually fail, restraint is.

Schelling called the underlying mechanism “the reciprocal fear of surprise attack” ⁵, and the security-dilemma literature has long studied how its severity depends on whether offense or defense has the advantage ⁶. Here that advantage is $q$.

Fig 1: The chain of suspicion and the game after exposure. Left: for identical civilizations, which equilibria exist at each base threat $\pi$ and strike success $q$. Right: the chain $r{n+1} = \pi + (1-\pi)F(r_n)$, with action thresholds spread around $1-q$. A spread of 0.5 around $q = 0.5$ is the original recurrence, which always climbs to 1. Drag the point, or change the spread, to see where the chain stops._

Proposition 4: Before Exposure, Hiding Dominates Revealing

Let the detection probability when civilization $c_i$ chooses to reveal be $\lambda_R$, and when it chooses to hide be $\lambda_H$, with $\lambda_R > \lambda_H$. Let the extinction risk once detected be $\rho_D$, and while undetected $\rho_0$, with $\rho_D > \rho_0$. Let $B_i$ be the cooperation benefits of public exposure and $C_i$ the operational cost of hiding.

$$U_i(\text{reveal}) = -[\lambda_R \rho_D + (1 - \lambda_R) \rho_0] M + B_i$$

$$U_i(\text{hide}) = -[\lambda_H \rho_D + (1 - \lambda_H) \rho_0] M - C_i$$

The difference:

$$U_i(\text{reveal}) - U_i(\text{hide}) = (B_i + C_i) - (\lambda_R - \lambda_H)(\rho_D - \rho_0) M$$

Therefore, hiding is better exactly when

$$(\lambda_R - \lambda_H)(\rho_D - \rho_0) M > B_i + C_i$$

(Lean: prop4_hide_iff).

The condition $\rho_D > \rho_0$ asks little. Even if every non-hostile civilization restrains itself after detection, the hostile share still strikes, so a detected civilization dies with probability at least $\pi q > 0$ (rhoD_pos). For any fixed $B_i$ and $C_i$, a large enough $M$ then makes hiding better (silence_for_large_M). Unlike preemption, silence does not depend on the chain of suspicion or on strikes usually succeeding. It needs only that some hostile civilizations exist and that broadcasting makes detection likelier. Even if broadcasting only slightly raises the probability of being found, the extinction loss makes broadcasting a losing bet.

6. Main Theorem

Definition (Dark Forest State): A system is in the Dark Forest state if for every civilization $c_i \in \mathcal{U}$, both of the following hold simultaneously:

1. Actively revealing one’s own location decreases its expected survival rate
2. Once mutually located with another civilization, restraint is not a risk-dominant strategy

Theorem (Sufficient Conditions for the Dark Forest): In a civilization system satisfying A1, A2, and B1–B5, with $0 < \pi < 1$ and $0 < q \le 1$:

1. Silence (robust): if broadcasting makes detection likelier ($\lambda_R > \lambda_H$) and $M$ is large enough, hiding is better than broadcasting (Proposition 4).
2. Preemption (conditional): after mutual detection, mutual striking is an equilibrium once $M > K_i/q^2$ (threshold_lt_one_iff). It is the only equilibrium when $\pi > r^\ast \approx 1 - q$ (only_striking). It is risk-dominant, and is the one selected when payoffs are observed with small noise, when $q > (1-\pi)/2$. Otherwise mutual restraint is the risk-dominant equilibrium (Proposition 3).
3. System level: under the replicator dynamics, in which each strategy reproduces in proportion to its fitness, silence spreads from any start whenever hiding is fitter (silence_spreads). Striking is bistable: it takes over when its initial share exceeds an edge $a^\ast = (r^\ast - \pi)/(1-\pi)$, and dies out below it (striking_takes_over, striking_dies_out). It has the larger basin, $a^\ast < 1/2$, exactly when it is risk-dominant (larger_basin_iff_risk_dominant), and with rare random mutations evolution spends almost all its time in the risk-dominant equilibrium ⁷. Lean checks this for best-reply dynamics: if every civilization best-replies to last round’s share of strikers and then switches with a small probability, then in a large enough population every stationary distribution puts almost all its weight on striking when striking is risk-dominant, and almost none when restraint is (kmr_stationary, kmr_selects_risk_dominant, kmr_selects_restraint). The same holds when civilizations revise one at a time: the stationary distribution is then unique, and almost all its weight falls on the state in which every civilization plays the risk-dominant action (seq_stationary_unique, seq_selects_risk_dominant, seq_selects_restraint). Section 9 tests the clause in a richer model.

The system is in the Dark Forest state when the first two hold with preemption selected, that is, when $q > (1-\pi)/2$. For identical civilizations with $\lambda_R > \lambda_H$, $\rho_D > \rho_0$ and a strike that costs something, the Dark Forest state holds for every large enough $M$ exactly then (dark_forest_state_iff). When strikes usually fail, the forest is still dark, because everyone hides, but it is no longer a hunting ground.

Proof sketch (backward induction):

• Endgame stage: once civilizations have located each other, the equilibria are those of Proposition 3. Which one is played depends on $\pi$ and $q$, not on how many levels of reasoning a civilization performs.
• Preceding stage: whichever equilibrium is played after detection, $\rho_D \ge \pi q > \rho_0$, so by Proposition 4 hiding dominates revealing for large $M$. One $M$ serves for every such equilibrium (silence_whatever_follows).
• Evolutionary level: this is a claim about dynamics rather than equilibrium. For the replicator dynamics it follows from the theorems in part 3; for richer dynamics, Section 9 checks it. $\square$

On uniqueness: the theorem does not assert a unique equilibrium. Mutual restraint remains an equilibrium whenever $\pi \le 1 - q$, and it is the better one for both sides. When $\pi < r^\ast < 1$ there are exactly three equilibria: none striking, all striking, and a mixed one in which the striking share is the edge $a^\ast$ of part 3 (stag_hunt_equilibria). What the Dark Forest adds is that, when strikes usually succeed, it is not the safe one.

7. Connections to Classical Theory

7.1 Isomorphism with the Hobbesian State of Nature

The Dark Forest Theory is structurally isomorphic to the “state of nature” described by Hobbes in Leviathan ⁸:

The key difference lies in the exit mechanism: Hobbes argued that rational individuals could escape the state of nature by entering a social contract, delegating authority to a sovereign to maintain order. In the Dark Forest, B1 (no supra-sovereign institution), B2 (unverifiable intentions), and B3 (light-speed lag making interaction frequency extremely low) jointly block the path to establishing a social contract. Hobbes’s “state of nature” has an exit; the Dark Forest (under the given conditions) does not.

7.2 Relation to the Fermi Paradox

The Fermi Paradox asks: if many civilizations exist in the universe, why have we observed no evidence of any?

The Dark Forest Theory offers one possible answer: civilizations exist, but silence is the equilibrium strategy. The absence of observable signals is not evidence that civilizations do not exist, but may instead indicate that civilizations are rationally hiding. By the theorem above, this half of the answer is the robust one.

However, this is only one of many candidate explanations for the Fermi Paradox ⁹. Others, such as the Great Filter ¹⁰, the Zoo hypothesis ¹¹ and extremely short civilizational lifespans, can equally account for observational silence without relying on the strong assumptions of the Dark Forest. From the single fact that “we have detected no signals,” it is impossible to determine which explanation is closer to reality.

8. Theoretical Limitations and Critiques

The above derivation is logically self-consistent within its assumption framework. However, each structural condition (B1–B5) can be challenged, and relaxing any one may fundamentally alter the equilibrium structure.

8.1 Fragility of the Unverifiable Intentions Assumption (Relaxing B2)

B2 assumes communication is completely untrustworthy. But game theory offers multiple mechanisms for breaking the cheap talk impasse:

Costly signaling: Conveying intention information by incurring an unforgeable cost (cf. Spence’s education signaling model ¹²). A civilization could send credible signals through irreversible self-disarmament, resource gifts, or technology disclosure. The key requirement: the cost of faking such signals must be high enough that hostile parties are unwilling to pay it. In a model with two types, benign civilizations signalling and hostile ones not is an equilibrium exactly when the signal costs a benign sender no more than trust is worth and a hostile sender at least as much (Lean: separating_iff). A signal then proves goodwill and silence proves hostility (separating_posterior, separating_silence); if both types signal, the signal again says nothing (pooling_posterior). Whether this is feasible at cosmic scales remains an open question.

Repeated games and reputation: If interactions between civilizations are repeated, the Folk Theorem shows that cooperation can be sustained as an equilibrium among participants with sufficiently high discount factor $\delta$ ². The Dark Forest indirectly suppresses $\delta$ through B3 (light-speed lag), but if two civilizations are close enough ($\tau_{ij}$ is sufficiently small), repeated-game cooperation remains theoretically viable.

Third-party arbitration and institutions: Adjudication by a super-civilization could partly substitute for credible commitments. B1 rules this out, but B1 is itself an empirical assumption, not a logical necessity. Consensus protocols of the blockchain kind are no way around it, since they need rounds of communication and so run into B3.

8.2 Questionability of the Technological Explosion Assumption (Relaxing B4)

B4 assumes high uncertainty in technological capability growth ($\sigma^2 > 0$). If $\sigma^2$ is constrained to be sufficiently small (i.e., technological development is smooth and predictable), then $\gamma \to 0$: with a random term of mean zero, $\gamma \le \sigma^2/c^2$, where $c$ is the gap, in logarithms, between the lethal level and the capability’s expected path (Lean: explosion_rare). The base threat then lies between $p$ and $p + \gamma$ (basePi_between), so $\pi \to p$, and the room for the chain of suspicion to unravel shrinks with it.

From an empirical standpoint: while human history has seen periods of accelerated technological development, there has never been an instantaneous jump spanning orders of magnitude. Technological development may face physical upper bounds (thermodynamic limits, speed-of-light constraints, computational complexity lower bounds), making infinite explosion physically impossible. On the other hand, this possibility cannot be ruled out either, since we have only one civilization as a sample.

8.3 Strike Costs and Exposure Risk (Relaxing B5)

The model assumes first strikes have a positive net-benefit interval (B5). But at cosmic scales:

• Interstellar strikes require enormous energy investments; $K_i$ may not be negligible relative to $M$.
• The act of striking may itself expose the attacker’s location to third-party civilizations $c_k$ (e.g., through observable energy-release signatures), increasing the attacker’s risk. This means $U_i(A)$ should include an additional penalty term for “exposure to third parties.” A recent paper argues that, once this is counted and no attacker can know it has found everyone, striking whatever one finds stops being an equilibrium whenever a strike is more visible to unseen civilizations than a hider is findable, while hiding remains one ¹³.
• If defensive technology significantly dominates offensive technology ($q \to 0$), first strikes almost never succeed, and the attack option no longer has positive expected payoff.

8.4 Absolutization of the Survival Axiom (Relaxing A1)

A1 sets survival as the lexicographically highest priority. But civilizations may have more complex value systems:

• They may be willing to accept some survival risk in pursuit of other goals (knowledge, aesthetics, moral principles).
• The “better to kill by mistake” logic driven by extreme risk aversion may itself be considered an unacceptable moral cost.
• If the utility function is not lexicographic but instead admits a finite rate of substitution among objectives, then the extinction loss $M$ is no longer “infinite,” and the model’s extreme conclusions soften significantly.

8.5 Complexity of Multi-Civilization Extensions

The two-player analysis cannot be directly extended to $n$-player games. In a multi-civilization environment:

• Coalition formation may alter the equilibrium structure. If multiple civilizations can form defensive alliances, a single civilization’s first strike faces coalition retaliation, reducing the expected payoff of an attack. Each ally lowers it further (Lean: uAttackAllied_anti), and with enough allies waiting beats striking whatever the other side does (coalition_deters).
• Signal externalities: Even if one civilization is destroyed, the observable signals produced by the attack (energy release, matter ejection) may be detected by third parties, exposing the attacker’s existence and location. This makes the net benefit of the attack strategy lower in multi-civilization environments than the two-player model predicts, and the lower the more third parties there are (uAttackSeen_anti).
• These effects make the optimality of “destroy upon discovery” no longer certain in multi-civilization environments, but the conclusion that “hiding is preferable” is strengthened, since exposure entails facing more potential adversaries. With each other civilization a potential attacker, the risk once detected grows with their number (rhoN_mono), so if hiding beats revealing among some number of civilizations, it does among more (silence_strengthens).

8.6 The Shape of the Chain of Suspicion

Proposition 2 shows that where the chain of suspicion stops depends on how action thresholds are distributed. The original linear recurrence needs thresholds spread over all of $[0, 1]$, including thresholds near zero: some non-hostile civilizations must be willing to strike at almost no fear. Remove them, and whenever the base threat lies below every civilization’s threshold, the chain stops at $\pi$. If some civilizations can never strike successfully, the chain can also come to rest partway, at a level of fear above $\pi$ but below certainty. In none of these cases does a large extinction loss change the picture, because it moves thresholds only down to $1 - q$.

8.7 What the Proofs Do Not Settle

Lean checks that each theorem follows from its assumptions. It relies on Lean’s kernel, on Mathlib at the pinned commit, and on three standard axioms (propext, Classical.choice, Quot.sound). Some questions are beyond any proof; others are only left out here.

Beyond any proof:

• Whether the model describes the universe. A1, A2 and B1–B5 are assumptions. With one known civilization and no observations of others, there is nothing to check them against, and no proof can supply that.
• Whether a theorem says what the sentence beside it says. Lean checks the formal statement, not its match with the prose. That match is checked only by reading the statements in the attached file, which is worth doing for any claim that matters to you.
• The readings the model builds in. Counting $\gamma$ into the strike probability assumes that a civilization able to destroy another is also willing to (Section 4.2). A1 enters as an additive utility with bounded gains and a large $M$. The global game uses the payoff normalized for large $M$, and lets $q$ range below 0 so that waiting dominates there. Enforcement in Proposition 0 (b) is an added chance of being destroyed, and the repeated game in (d) has abstract payoffs. The models of Sections 8.1 and 8.5 are the simplest that make their points: two types and one signal; strikes, sightings and allies that act independently. In the dynamics with mutations, a population exactly at the tipping share counts as waiting, and when civilizations revise one at a time, a mistake plays the opposite action. A2 never enters the model at all, so its role in the conclusion is an informal reading. Throughout the main argument there are two civilizations. Each of these choices can be argued for or against, not proved.
• Whether B1–B5 are logically independent. Each is shown to be used (each_condition_used), but whether informal conditions are independent of one another is not a formal question.
• The simulation. Section 9 reports twelve runs per setting of two models. In the reasoning one, civilizations apply Propositions 3 and 4, but the world, with one-sided detection, learned beliefs and growth, is not the one the theorems describe, and its settings are ours. Among them are the prior that almost no one strikes, a Beta(0.1, 20); the age of 100 steps at which a civilization counts as established; and the strike cost $K/M = 0.0005$, on which its preemption depends. It illustrates; it cannot prove.
• The analogies of Section 7. The comparisons with Hobbes and with the Fermi paradox are interpretations.

Not proved here, though they could be: the parts of the cited theorems beyond the classes checked above.

• Carlsson and van Damme ⁴ for two-by-two games in which the state changes how much the other side’s action matters, and for different payoffs on the two sides under priors other than flat. Lean checks every game in which the state shifts a side’s gain by the same amount whatever the other does.
• Kandori, Mailath and Rob ⁷ for their whole class of dynamics. Lean checks the two standard best-reply dynamics, simultaneous and one at a time; the general class needs the Markov chain tree theorem, which is not yet in Mathlib.
• The folk theorem of Fudenberg and Maskin ², which sustains any individually rational payoff with minmax punishments. Lean checks Friedman’s version, which sustains any pure profile that pays everyone more than a stage Nash equilibrium.

9. A Simulation

Figure 2 runs two models of a small universe. In the first, behaviours are inherited and culled, which tests the theorem’s system-level clause. In the second, civilizations decide by Propositions 3 and 4, which tests whether the behaviours the theory derives appear when civilizations reason as it says, in a world closer to the novel’s.

Selection. One hundred civilizations live on a torus, each at a random position for its lifetime. Each has two heritable traits: whether it broadcasts, and whether it strikes whatever it detects. A share $p$ is hostile and strikes whatever it detects regardless. A civilization within range can detect another only after light from it has had time to arrive, and then detects it with probability $\lambda_R$ per step if it broadcasts and $\lambda_H \ll \lambda_R$ if it hides. Strikes travel at light speed and succeed with probability $q$. A failed strike reveals the attacker to its target, which strikes back, and any strike exposes the attacker to everyone else with probability $e$. Civilizations also die of other causes, at a low rate. Dead slots are refilled by offspring of the survivors, drawn in proportion to one plus $B$ times their number of peaceful contacts, so contact pays; traits mutate at 2% per birth. Two assumptions are built in: the population stays at one hundred, since every death is followed by a birth, and newcomers copy the strategies of survivors. This is selection acting on strategies, the reading of the replicator dynamics, not an account of how civilizations arise.

Over twelve runs with fixed seeds for each setting, each of 3,000 steps:

• Silence spreads whenever hostile civilizations exist. With the defaults ($p = 0.1$, $q = 0.7$), broadcasting falls from 70% of civilizations to at most 5% in every run, as Proposition 4 predicts.
• Striking spreads only in a hunting ground. With the defaults it dies out, to at most 2% in every run, even though with $\pi = p = 0.1$ the strike success $q = 0.7 > (1-\pi)/2 = 0.45$ makes striking the risk-dominant response after mutual detection. In this universe detection is rarely mutual: striking what you find mostly kills civilizations that had not found you, and the failed strikes and exposures cost the striker more than the rare preempted threat saves. The game played here is therefore not the stag hunt that the replicator theorems describe, which is why the two disagree. Striking survives only when hostile civilizations are common, strikes almost always succeed, and strikes are invisible to others ($p = 0.3$, $q = 0.95$, $e = 0$). There it holds between 15% and 85% of non-hostile civilizations in eleven of twelve runs, and a majority in four.
• Without hostile civilizations, and with enough to gain from contact, the forest stays lit. With $p = 0$ and $B \ge 1$, most civilizations keep broadcasting.

While traits mutate, the state never settles, but its statistics do. Over 30,000 steps with four seeds, the defaults keep broadcasting at 0–1% and striking at 1–3% in every 3,000-step window, while in the hunting ground striking wanders between 17% and 79% from one window to the next. With mutation switched off there are absorbing states, reached within 3,000 steps: broadcasting always dies out, and in the hunting ground striking ends at all or nothing, all in one run of four and nothing in three, the bistability of the replicator theorems.

Reasoning. Here civilizations arise independently, at random places and times, and only where no living civilization’s territory already lies, so the finite universe of A2 sets how many there are. A newcomer is small, and hostile with probability $p$, a type no one else can see (B2). Capability grows on resources shared with overlapping neighbours, territory grows with it, and a larger civilization is easier to find, whether it hides or not. With a small probability per step, capability jumps fivefold (B4). Finding, strikes and exposure work as in the first model, with the same light delays (B3), but a strike succeeds more often the more capable the attacker is relative to its target (B5). Each civilization learns from what it sees: of the civilizations it has found and not struck itself, the share destroyed by a strike within a horizon, starting from the belief that almost no one strikes. It then decides by the post’s formulas: it hides when Proposition 4 says so, and on finding another it strikes when Proposition 3 says so, extended to one-sided detection, unequal capability and exposure. Hostile civilizations strike whatever they find. The figure’s source states the rules in full.

Over twelve runs with fixed seeds for each setting, each of 3,000 steps:

• Silence is learned. Established civilizations, those that have lived 100 steps, mostly hide: a median of 10% broadcast. Those that hide have seen strikes, with a median belief of 0.13 that a found civilization is destroyed, while those still broadcasting are still at their prior of 0.005. With beliefs frozen at the prior, every civilization broadcasts.
• Preemption follows the capability gap. A non-hostile civilization strikes 68% of the civilizations it finds that are at least five times smaller, 60% of those two to five times smaller, 1% of its peers, and none that are larger: a median of 36% of all it finds. Peers wait, as in the first model, because striking an equal risks a return strike. The weak are struck because striking them costs almost nothing: success is nearly certain, and the return strike weak. So preemption does not need hostile civilizations; without any, the median is 37%. It needs strikes that cost the strong little, here $K/M = 0.0005$: at $K/M = 0.05$ it stops, at a median of 1%, which is the $K/(qM)$ term of Proposition 3 doing what it says. Technological explosion doubles it (a median of 18% without), visible strikes cut it (14% at $e = 0.6$), and learning adds to it (14% with beliefs frozen at the prior).
• Newcomers rarely survive. They arrive broadcasting, since their prior says it is safe, and a median of 13% live 100 steps; most are found and struck before they have found anyone. About 20 civilizations are alive at a time.
• Without growth, the forest is quiet and peaceful. With capabilities fixed and equal, a median of 1% of established civilizations broadcast, none strikes first, 87% of newcomers survive, and about 160 civilizations are alive.

This universe settles in the same sense as the first: births and deaths never stop, but over 30,000 steps with four seeds the share of findings that end in a strike stays between 30% and 42% in every 3,000-step window, with about 20 civilizations alive; without growth, about 160, and silent.

The two models agree on silence and differ on preemption. Under selection, striking what one finds rarely pays, because those found rarely know about the finder. With reasoning and growth it pays against the small, and the forest of the novel, in which the grown clear away the young, appears when capabilities differ and strikes are cheap for the strong, whether or not anyone is hostile. Neither model is the world the theorems describe: detection is rarely mutual, beliefs are learned rather than given, and in the second, capability grows. Both leave out coalitions, movement and cosmic scale, and the first also leaves out growth and technological explosion. They illustrate; they are not evidence about the universe.

Fig 2: A small dark forest, in two modes. Dots are civilizations: navy ones broadcast, grey ones hide, and a ring marks hostile ones and those that strike (in the reasoning mode, those that have struck first). Faint discs are territories, lines are strikes in flight, and spreading rings are strikes that hit. In the selection mode the chart tracks the share that broadcasts and the share of non-hostile civilizations that strike; in the reasoning mode, the share of established civilizations that broadcast, the share of findings that end in a first strike, and the share of newcomers that live their first 100 steps. The presets set the parameters for the cases in the text; the sliders change them. The numbers are illustrative, not data.

10. Conclusion

Translating the Dark Forest Theory of Three-Body Problem into rigorous game-theoretic form yields a clearer, and more circumscribed, conclusion:

The two axioms “survival priority” and “finite resources” alone are insufficient to derive the Dark Forest. With the structural conditions B1–B5 added, the Dark Forest’s two halves come apart. Silence follows under weak conditions: some hostile civilizations, and a detection advantage for those who hide, are enough given a large extinction loss. Preemption is conditional: after mutual detection, striking and restraint are both equilibria, and striking is the risk-dominant one only when strikes usually succeed, $q > (1-\pi)/2$. The chain of suspicion, in the form the novel gives it, does not by itself carry fear to certainty. Finite resources (A2) never enters the formal model. Read informally, it acts as an amplifier: competition for resources plausibly raises $\gamma$ and with it the base threat, making the forest easier to darken, though nothing above proves this (Section 8.7).

The Dark Forest is a stable equilibrium under specific conditions, but it is not the universe’s only possible fate. It provides sufficient conditions, not inevitability. Relaxing any one of B1–B5 may open a path toward cooperative equilibrium.

Thus, the Dark Forest Theory is less a moral judgment that “all civilizations in the universe are evil” than a cooler structural proposition:

In a universe where extinction cost overrides all else, intentions cannot be credibly verified, and communication delay renders repeated games ineffective, silence is more stable than goodwill.

Note: The formalization in this article is a theoretical reconstruction of the novel’s text, not Liu Cixin’s own formulation. Cosmic sociology as a discipline does not actually exist; its “axioms” can be neither verified nor falsified. The Lean file checks the mathematics of the model, not whether the model describes any real universe.

Revised on September 27, 2026. Proposition 2 previously claimed that the chain of suspicion drives threat to certainty whenever $\pi > 0$, which holds only for uniformly spread thresholds; its note on robustness had the effect of a large $M$ backwards. Section 4.2 derived $\gamma > 0$ from positive variance alone, which does not suffice. Proposition 3’s utilities are now symmetric, Section 1 states when the additive utility represents A1’s order, the main theorem separates silence from preemption, the formal claims, including the counterexamples of Proposition 0, equilibrium selection in the global game for every equilibrium and every smooth prior, long-run selection under the replicator dynamics and under mutations, and the cited theorems of Friedman, of Carlsson and van Damme, and of Kandori, Mailath and Rob for broad classes of games, are checked in Lean, Section 8.7 says what the proofs cannot settle, and Section 9 adds a simulation in two modes, one in which behaviours are selected and one in which civilizations reason by the theory’s own rules.