Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Theorem 2.7: reduction to a Nice Devil

Proved
AngelDevil.nice_devil_reduction

by Yuxuan Xu · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

angel-problemcombinatoricsgame-theory

For every positive integer power, if the Angel has no winning strategy, some Nice Devil can keep every finite safe play in a fixed box of positive integer radius. This formulation includes the determinacy observation from the introduction in addition to Theorem 2.7.

Preamble
import Definitions.Def_AngelDevil_Game
Formal statement
theorem AngelDevil.nice_devil_reduction (p : Nat) (hp : 0 < p) : ¬ AngelDevil.AngelWins p → ∃ N, 0 < N ∧ AngelDevil.NiceCanConfine p N := by sorry
Source
Andras Mathe, The Angel of power 2 wins, CPC 16 (2007), 363-374; https://doi.org/10.1017/S0963548306008303; author manuscript internal pagination. Theorem 2.7, manuscript p. 3, with the introductory determinacy observation on p. 1.
Read-back

What the Lean code literally says, in plain math · gpt-6

For every positive natural number p, assume that there does not exist a total Angel strategy that survives against every total Devil strategy, where points are integer pairs, the Angel starts at (0,0), a Devil strategy maps each finite list of Angel positions to either a point or a pass, and an Angel strategy maps that position list together with the list of Devil responses to its next point. In each round the Devil responds first, and the Angel then responds after seeing that response; survival means that in every round each coordinate changes by at most p in absolute value and the new point is unequal to all points selected by the Devil so far, including in that round. Then there exist a positive natural number N and one Devil strategy D such that (i) for every nonempty finite position list starting at (0,0) with all consecutive coordinate changes at most p in absolute value, any point selected by D is different from (0,0) and has a coordinate difference of absolute value greater than p from each position occurring before the last entry, and (ii) for every total Angel strategy A and every natural number n, if all first n rounds of the recursively defined play of A against D satisfy the stated movement and avoidance conditions, then both coordinates of its position after n rounds lie in [−N,N]. Passes and repeated selections are permitted; D has no restrictions on position lists failing the stated journey condition, while on the singleton origin list it is only forbidden to select the origin. Staying still is a permitted jump. The strategies and play are total, including after failures; the confinement conclusion concerns every finite safe prefix, whether or not it extends to infinite survival. At n = 0 its premise is empty and its conclusion concerns the origin. The assumption rules out a single universally surviving Angel strategy; it does not itself posit a single universally defeating Devil strategy.

Human review
  • Endorsed by Shuze Chen · Oct 18, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Yuxuan Xu · Oct 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me