Mathematics

The Mathematics of Taikyoku Shogi

A formal model, exact counts from the engine, and a roadmap to a machine-checked formalization in Lean 4.

Abstract · 1 Model · 2 Counts · 3 State space · 4 Game tree · 5 Mobility · 6 Rank algebra · 7 Symmetry · 8 Complexity · 9 Lean roadmap · 10 AI and solving · 11 Open problems · References

Working draft. Every number marked V was computed by the game's own rules engine and is reproducible with godot --headless --path . -s tests/math_stats.gd. P marks short proofs given here, C results cited from the literature, O open or conjectural statements and L statements planned for a machine-checked proof in Lean 4. The Lean development has not been written yet; the code blocks below are statements we intend to prove, not compiled theorems.

Abstract

Taikyoku shogi is the largest known shogi variant: two armies of 402 pieces on a \(36\times 36\) board, drawn from 301 piece kinds with move rules that include unbounded riders, jumpers, two-step “area” moves, 90° turning “hook” moves and multi-capture “range” moves. We give a formal model of positions and legal moves, exact initial-position counts (\(97\) legal first moves; \(1{,}426{,}099\) positions after three plies), upper bounds on the size of the state space (\(<10^{3604}\)) and a measured branching factor (\(\approx 320.6\) in random play), closed forms for the mobility of riders on an \(N\times N\) board, and a rank algebra for range capture. We then state the theorems we plan to formalize in Lean 4, describe how we are working to make the AI stronger and to solve as much of the game as can be solved, and list open problems.

1. A formal model

1.1 Board, sides, pieces

Definition 1 (board). Fix \(N=36\). The board is \(B=\{0,\dots,N-1\}^2\), so \(|B|=N^2=1296\). A square is \(p=(x,y)\); the two sides are \(\mathsf B\) (Black, moves first) and \(\mathsf W\), with \(\bar{\mathsf B}=\mathsf W\), \(\bar{\mathsf W}=\mathsf B\). Black advances towards increasing \(y\); White towards decreasing \(y\).
Definition 2 (piece kinds). Let \(K\) be a finite set of piece kinds with a rank function \(\rho:K\to\mathbb N\cup\{\infty\}\) and a set of royal kinds \(R\subseteq K\) with \(\rho(k)=\infty\) for \(k\in R\). A kind \(k\) may have a promotion \(\mathrm{pr}(k)\in K\cup\{\bot\}\). In our data \(|K|=301\) V, of which 209 occur in the initial position and 92 occur only as promotions. The royal kinds are the King and the Crown Prince.
Definition 3 (position). A position is a pair \(s=(\pi,t)\) with \(\pi:B\to\{\varnothing\}\cup(K\times\{\mathsf B,\mathsf W\})\) and \(t\) the side to move. The set of all positions is \(\mathcal S\). The initial position \(s_0\) places 402 pieces for each side in the 12 ranks nearest that side, with a gap of 12 empty ranks between the armies. One rank of each army holds 6 pieces and each of the other 11 ranks is full (\(6+11\cdot 36=402\)) V. The multiplicities of kinds in the setup are: one kind \(\times 36\) (the pawn), one kind \(\times 4\), 155 kinds \(\times 2\) and 52 kinds \(\times 1\) (\(36+4+2\cdot 155+52=402\)) V.
00121224243535file xrank yBlack (moves first)White12 empty rankspawns (36)
Figure 1. The initial position (drawn from the setup table in the game data). Black (dark) fills ranks 0–11 and White (red) fills ranks 24–35, rotated by 180°; the lighter cells are the 36 pawns of each side. Twelve ranks are empty between the armies.

1.2 Moves as set-valued functions

Write \(\mathrm{Own}_t(\pi)\) and \(\mathrm{Opp}_t(\pi)\) for the squares occupied by the side to move and by its opponent, and orient direction vectors by the mover (\(d\mapsto d\) for Black, \(d\mapsto -d\) for White). A move is a finite path \(p=q_0\to q_1\to\cdots\to q_m\) together with the set \(C\) of captured squares. A kind's move rule is a finite union of the following components.

Slide \(\mathrm{Sl}(d,\ell)\), \(d\in\mathbb Z^2\), \(\ell\in\{1,\dots,N-1\}\cup\{\infty\}\): \(\{\,p+jd\ :\ 1\le j\le \ell,\ p+id\in B\ \forall i\le j,\ \pi(p+id)=\varnothing\ \forall i<j,\ p+jd\notin\mathrm{Own}_t\,\}\), capturing \(p+jd\) if it is in \(\mathrm{Opp}_t\). (A step is \(\ell=1\); a rider has \(\ell=\infty\).)
Leap \(\mathrm{Lp}(v)\): the single square \(p+v\) if it is on the board and not in \(\mathrm{Own}_t\); intermediate squares are ignored.
Jump-slide \(\mathrm{JS}(d,s,\ell)\): jump over the first \(s\) squares in direction \(d\) (whatever they contain), then land on or slide up to \(\ell\) squares along \(d\), stopping at the first occupied square as for a slide.
Hook \(\mathrm{Hk}(d)\): slide along \(d\), optionally turn \(90^\circ\) once at any empty square on the way, and continue sliding in the new direction.
Area move (lion family): up to two single steps in any of the 8 directions in one turn, each of which may capture, the two steps not necessarily collinear; plus a jump to any square at distance two, a capture of a neighbour without moving, and a pass. A move records its intermediate square \(q_1\).
Range capture \(\mathrm{RC}(d,r)\), \(r\in\mathbb N\): see Section 4.

The set \(\mathrm{Mv}(s)\) of legal moves of a position is the union over the mover's pieces of their components' moves. There is no check rule: a move is legal exactly when it is generated. A player wins by capturing every enemy royal piece. Promotion is a rule parameter: on entering the far 11 ranks (default), on first capture, or never.

In the implementation a move is the triple \((\text{from},\text{to},\text{via})\). Distinct values of \(\text{via}\) are counted as distinct moves, which is why counts below exceed the number of (from,to) pairs.

Slide Sl(d, ∞)Leap Lp(v)Jump-slide JS(d, 2, ∞)Hook Hk(d)↰Area move (lion)12Range capture RC(d, r)31215may movecapturedmoverenemyblocker / own
Figure 2. The six move components of Section 1.2 on a \(9\times9\) board (schematic). The slide stops at the first piece and may capture it; the leap ignores the piece in between; the jump-slide hops two squares; the hook turns once at any empty square; the area move takes up to two steps; the range capture passes over lower-ranked pieces and takes all of them.

2. Exact counts from the initial position

Definition 4 (perft). \(\mathrm{perft}(s,0)=1\) and \(\mathrm{perft}(s,n)=\sum_{m\in\mathrm{Mv}(s)}\mathrm{perft}(s\cdot m,\,n-1)\).
\(n\)\(\mathrm{perft}(s_0,n)\)ratio to previous
197-
29,39396.8
31,426,099151.8
10^010^110^210^310^410^510^610^797n = 19,393n = 21,426,099n = 3dashed: 97ⁿ (if every ply offered 97 moves)perft(s₀, n)
Figure 3. Exact node counts \(\mathrm{perft}(s_0,n)\) on a logarithmic axis. The dashed marks are \(97^n\); the true counts grow slightly faster than \(97^n\) from \(n=3\) as lines open up.

V The opening has \(97\) legal moves for Black. Note \(\mathrm{perft}(s_0,2)=9393\) is \(16\) below \(97^2=9409\): White's number of replies depends slightly on which move Black played (the mean is \(9393/97\approx96.8\)).

Statement for Lean: L theorem perft_one : (moves init).card = 97, and likewise perft init 2 = 9393, perft init 3 = 1426099, checked first by decide/native_decide and then, if the kernel allows it in reasonable time, by a proof that avoids the compiler (see Section 8).

3. Size of the state space

Proposition 1 (crude bound). \(|\mathcal S|\le 2\,(1+2|K|)^{N^2}\); with \(|K|=301\) and \(N=36\), \(\log_{10}|\mathcal S|<3604\). P
Proof. Each square holds one of \(1+2|K|\) values and there are two sides to move. \(\square\)
Proposition 2 (initial placements). The number of ways to place the two initial armies (as multisets of kinds, 402 pieces each) on the empty board is \[\frac{1296!}{(1296-804)!\;\prod_{k}\big(m_k!\big)^2}\;\approx\;10^{2181},\] where \(m_k\) is the multiplicity of kind \(k\) in one army. P (a multinomial coefficient; the exponent is computed exactly from the setup table)

Both numbers dwarf the figures usually quoted for other games (as tabulated by Allis, 1994): chess \(\approx10^{46}\), shogi \(\approx10^{71}\), Go \(\approx10^{172}\) positions C. A far better bound should exist because reachable positions have at most 804 pieces and captures are irreversible, but any such bound remains astronomically beyond exhaustive enumeration.

Chess10^46Shogi10^71Go10^172Taikyoku: initial placements10^2181Taikyoku: upper bound10^3604log₁₀ of the number of positionschess, shogi, Go: as tabulated by Allis (1994). Taikyoku: this page, Section 3.
Figure 4. State-space sizes on a logarithmic scale. The two Taikyoku bars are mathematical bounds (placements of the starting armies, and the crude bound of Proposition 1), not counts of reachable positions.

3.1 Endgame tablebases are within reach

For a King and one other piece against a bare King the number of placements is \(1296\cdot1295\cdot1294\cdot 2=4,343,492,160\) P (ordered placements of three distinct pieces, times side to move). That is about \(4.3\times10^{9}\) states: small enough that exhaustive retrograde analysis of such endgames is a realistic computation, and would give exact distance-to-win tables for every piece kind. O We have not computed them.

4. Branching factor and game-tree size

We measured the number of legal moves along random playouts (3,600 positions over 30 playouts of up to 120 plies, fixed seed) V:

plies0–1920–3940–5960–7980–99100–119
mean legal moves203.0267.8307.4349.8382.9412.9
150250350450203.00–19267.820–39307.440–59349.860–79382.980–99412.9100–119ply numbermean legal moves
Figure 5. Mean number of legal moves along random playouts, by ply range (30 playouts, fixed seed). The count rises as the board opens up.

The overall mean is \(\bar b\approx 320.6\) with a maximum of 608. The growth with the ply number reflects the board opening up as pieces are captured and the riders gain open lines. (Random play is not representative of strong play, so \(\bar b\) is a rough scale, not an estimate for good players.)

Following Allis, a game-tree complexity estimate is \(\bar b^{\,d}\) for an average game length of \(d\) plies. The length of a real game is unknown, so we tabulate:

\(d\) (plies)\(\log_{10}\bar b^{\,d}\)
100251
200501
4001002
8002005
01002003004000200400600800Chess 10^123Shogi 10^226Go 10^360game length d (plies)log₁₀ b^db ≈ 320.6
Figure 6. The Allis-style estimate \(\log_{10}\bar b^{\,d}\) against the unknown game length \(d\); the dashed lines are the commonly quoted game-tree sizes of chess, shogi and Go.

For comparison Allis gives \(\approx10^{123}\) (chess), \(10^{226}\) (shogi) and \(10^{360}\) (Go) C. Even a short game of 200 plies exceeds all three.

5. Mobility and piece value

Definition 5. The mobility \(\mu(k,p)\) of kind \(k\) at square \(p\) is the number of legal moves of a lone \(k\) at \(p\) on an otherwise empty board. The game's evaluation function uses \(v(k)=10+2\,\mu(k,c)\) where \(c=(18,18)\) is a central square (royals are given a constant dominating value).

V Over the 301 kinds: minimum \(\mu=1\), median \(43\), mean \(70.0\), maximum \(2,520\). The maximum is attained by the Hook mover, whose turning paths multiply the count: \(\mu\) counts moves \((\text{from},\text{to},\text{via})\), so one destination reached by several turning squares is counted several times. (The number of distinct destination squares is smaller; see Section 9, M6.)

010203040506070809010011142–3334–7308–152616–318032–639564–12718128–2554256+mobility μ (moves from the centre)number of piece kindsred: contains the rook (70); blue: contains the bishop's mean (46)
Figure 7. Distribution of the mobility \(\mu\) over the 301 piece kinds, in doubling bins (the last bin collects all kinds with \(\mu\ge256\)). The red bar contains the rook value 70 and the blue bar the bishop's mean 46.
Proposition 3 (rook). On an empty \(N\times N\) board a rook has exactly \(2(N-1)\) moves from every square. Hence its mean mobility is \(2(N-1)=70\) for \(N=36\). P
Proof. From \((x,y)\) there are \(x+(N-1-x)\) horizontal and \(y+(N-1-y)\) vertical squares: \((N-1)+(N-1)\). \(\square\)
Proposition 4 (bishop). The mean mobility of a bishop over all squares of an empty \(N\times N\) board is \[\bar\mu_{\mathrm{B}}(N)=\frac{2(N-1)(2N-1)}{3N},\qquad \bar\mu_{\mathrm B}(8)=8.75,\quad \bar\mu_{\mathrm B}(36)=\frac{2\cdot35\cdot71}{108}\approx 46.02.\] P
Proof. From \((x,y)\) the number of squares reachable in direction \((+1,+1)\) is \(\min(a,b)\) with \(a=N-1-x\), \(b=N-1-y\); the other three diagonal directions are the same after reflecting the board, so \(\bar\mu_{\mathrm B}=\tfrac{4}{N^2}\sum_{a,b=0}^{N-1}\min(a,b)\). The number of pairs \((a,b)\) with \(\min(a,b)=m\) is \((N-m)^2-(N-m-1)^2=2(N-m)-1\), hence \[\sum_{a,b}\min(a,b)=\sum_{m=0}^{N-1}m\,(2(N-m)-1)=(2N-1)\tfrac{N(N-1)}{2}-2\tfrac{(N-1)N(2N-1)}{6}=\tfrac{(N-1)N(2N-1)}{6}.\] Multiplying by \(4/N^2\) gives \(\tfrac{2(N-1)(2N-1)}{3N}\). \(\square\)
6935bishop movesmean 46.02(a rook has 70 everywhere)
Figure 8. Bishop mobility at every square of an empty \(36\times36\) board. It is smallest on the edge and largest in the centre; its average is exactly \(\frac{2(N-1)(2N-1)}{3N}\) (Proposition 4).

The mean mobility of a queen (rook + bishop) is therefore \(\approx 70+46.02=116.02\) on this board. The ratio of mean mobilities rook : bishop is \(70/46.02\approx1.52\), close to the classical chess convention \(5:3.25\approx1.54\); this is suggestive but not a derivation of piece values, because blockers are ignored. A mobility model with occupancy (a random density \(\delta\) of blockers, giving geometrically distributed ray lengths) is a natural refinement. O

6. Range capture and the rank algebra

Definition 6 (range capture). Let \(d\) be a direction and \(r\in\mathbb N\) a rank. For a position \(\pi\), set \(J=\max\{\,j\ge 0 : \forall i\le j,\ p+id\in B \text{ and } (\pi(p+id)=\varnothing \text{ or } \rho(\mathrm{kind}\,\pi(p+id))<r)\,\}\). \(\mathrm{RC}(d,r)\) consists of the moves from \(p\) to any empty or capturable square \(p+jd\), \(1\le j\le J\), that capture every occupied square among \(p+d,\dots,p+jd\), whether friend or foe. The \(r\) of a kind is its capture rank.
3121524capturer, rank r = 3rank 5 ≥ r: stops the rayJ = 4: squares passed over (ranks < 3)the move captures every piece it passes: here the pieces of rank 1, 2 and 1
Figure 9. A range capture of rank \(r=3\). The ray passes over pieces of rank 1, 2 and 1, capturing all of them (red), and is stopped by the piece of rank 5 (grey). Empty squares on the way (green) are just passed.
Lemma 1 (untouchable by range capture). If a move in \(\mathrm{RC}(d,r)\) captures a piece of kind \(k\) then \(\rho(k)<r\). In particular, because royals have \(\rho=\infty\), no range capture ever captures a royal piece. \(\mathrm{RC}\) moves capture at most \(N-1=35\) pieces. P L
Proof. Captured squares lie among \(p+id\), \(i\le J\), all of which satisfy \(\rho<r\) by definition of \(J\); a ray has at most \(N-1\) squares. \(\square\)
Lemma 2 (monotonicity). For fixed \(p,d,\pi\), if \(r\le r'\) then \(J(r)\le J(r')\) and the set of squares passed over under \(r\) is a prefix of that under \(r'\). Hence a higher-ranked range capturer weakly dominates a lower-ranked one with the same directions. P L
Proof. The predicate defining \(J\) becomes weaker as \(r\) grows. \(\square\)

Planned Lean form.

-- sketch, not yet compiled
inductive Side | black | white
structure Pos where
  board : Fin 36 → Fin 36 → Option (Kind × Side)
  turn  : Side

def rangeCapturePassed (π : Pos) (p : Fin 36 × Fin 36) (d : Int × Int) (r : Nat) : List (Fin 36 × Fin 36) := ...

theorem rangeCapture_rank_lt {π p d r c} (hc : c ∈ captured (rangeCapture π p d r)) :
    rank (kindAt π c) < r := by ...

theorem royal_untouchable {π p d r c} (hc : c ∈ captured (rangeCapture π p d r)) :
    ¬ isRoyal (kindAt π c) := by ...

theorem rangeCapture_card_le {π p d r} : (captured (rangeCapture π p d r)).length ≤ 35 := by ...

7. Symmetries and invariants

Proposition 5 (colour symmetry). Let \(\tau(x,y)=(N-1-x,\,N-1-y)\) (rotation by \(180^\circ\)) and extend it to positions by swapping colours. The initial position is \(\tau\)-invariant P (both armies are generated from the same setup table), and \(\tau\) maps legal moves of \(s\) bijectively to legal moves of \(\tau s\) (the move rules are defined relative to the mover). In particular \(\tau\) maps \(\mathrm{Mv}(s)\) bijectively onto \(\mathrm{Mv}(\tau s)\), so \(|\mathrm{Mv}|\) agrees on \(\tau\)-related positions. L

The setup is not left–right symmetric (only 2 of its 12 ranks read the same in both directions) V, so there is no reflection symmetry of the initial position to exploit.

Invariants to prove. L (i) the number of pieces of each side never increases except by the moving side's captures; (ii) a piece promotes at most once along its history (promoted kinds have \(\mathrm{pr}=\bot\)); (iii) under the default rule a piece promotes only when its move enters or ends in the promotion zone; (iv) the game is over iff a side has no royal piece; (v) \(\mathrm{Mv}(s)=\varnothing\) is possible (a side may have no legal move) and its outcome must be specified.

8. Complexity-theoretic context

For \(n\times n\) generalizations, chess is EXPTIME-complete (Fraenkel & Lichtenstein, 1981), shogi is EXPTIME-complete (Adachi, Kamekawa & Iwata, 1987) and Go under Japanese rules is EXPTIME-complete (Robson, 1983) C. Taikyoku shogi is a single finite instance, so asymptotic classes do not apply to it directly. We conjecture that the family of games obtained by letting \(N\) grow with the setup scaled accordingly (and a fixed repertoire of the component moves above) is also EXPTIME-complete: the natural route is a reduction from a generalized shogi position, since every shogi piece is a Taikyoku component. O We have no proof.

Infinite play. The rules as implemented contain no repetition or move-limit rule, so the game graph has cycles and the value of a position is defined by the usual retrograde fixpoint (win/loss in a finite number of plies, otherwise draw by infinite play). Formalizing this in Lean needs an inductive predicate WinIn : Nat → Pos → Side → Prop and a coinductive notion of avoiding loss. L

9. Roadmap: a machine-checked formalization in Lean 4

We intend to develop the model above in Lean 4 (de Moura & Ullrich, 2021) so that every V and P statement on this page becomes a theorem checked by the kernel, and every counting claim is tied to the same data the game executes. Planned milestones:

  1. M1 – Data. Import the 301 kinds (Betza-style move descriptions) as a Lean structure; prove the generated component tables equal the ones the engine uses.
  2. M2 – Positions and moves. Define Pos, the component move functions (slide, leap, jump-slide, hook, area, range capture) and moves : Pos → Finset Move; prove soundness (every move is on the board, never captures an own piece except in range capture, never captures a royal by range capture).
  3. M3 – Perft. perft init 1 = 97, perft init 2 = 9393 by decide; perft init 3 = 1426099 by a verified efficient implementation (refinement proof from the naive moves). A kernel-checked proof of \(n=3\) without native_decide is a serious computation (about \(1.4\times10^{6}\) leaves) and may need a bespoke reflection proof.
  4. M4 – Invariants. Items (i)–(v) of Section 7.
  5. M5 – Rank algebra. Lemmas 1 and 2, then the statement that range capture is the unique move component that can capture more than 2 pieces.
  6. M6 – Closed forms. Mean mobility of riders (Propositions 3 and 4), generalized to arbitrary direction sets \(D\subseteq\{-1,0,1\}^2\), with decide checks for \(N=8\) and \(N=36\).
  7. M7 – Symmetry. Proposition 5 and its consequences for outcome classes.
  8. M8 – Game theory. Outcome predicate by retrograde induction, correctness of a small endgame solver (King + one piece vs King), and the claim that for each kind the tablebase value is computable within the \(4.3\times10^{9}\) bound.
M1 DataM2 Positionsand movesM3 PerftM4 InvariantsM5 RankalgebraM6 ClosedformsM7 SymmetryM8 Gametheory
Figure 10. Dependencies between the planned Lean milestones M1–M8 of Section 9.

Beyond formulas we expect Lean to expose subtle points in the sources: where the surviving rule descriptions disagree (promotion, hook moves, area-move edge cases) the formal definitions will force a choice, and we will publish each choice as a labelled rule parameter.

10. Making the AI smarter, and solving the game

What the AI is today. The computer opponent is an iterative-deepening alpha-beta search with killer and history move ordering, quiescence search at the hardest level and a time budget (1.5 s at Normal, 3 s at Hard). Its evaluation is material weighted by the mobility value of Section 5, \(v(k)=10+2\mu(k,c)\), plus positional terms (advancement and pressure on the enemy royals). It is far from strong: with a branching factor of \(\approx 320.6\) (Section 4) a search of fixed time reaches only a few plies.

Our goals. We are working to make the AI substantially smarter and, as far as mathematics allows, to solve the game. Following Allis, a game is ultra-weakly solved when the value of the initial position is known, weakly solved when a strategy achieving that value from the initial position is known, and strongly solved when the value of every position is known. Strong solution is impossible here: Section 3 bounds the state space only by \(10^{3604}\), and even the placements of the two initial armies number \(\approx10^{2181}\). Weak or ultra-weak solution of the full game is also far beyond brute force at today's computing power, so our program is staged:

  1. Search engineering. Transposition tables with Zobrist hashing, better move ordering, null-move and late-move reductions, and a faster move generator (the current generator is written for clarity, not speed: it takes about 20 s to enumerate the \(1.4\times10^6\) leaves of \(\mathrm{perft}(s_0,3)\)). Every optimization will be checked against the reference perft numbers of Section 2.
  2. Learned evaluation. Replace hand-set mobility values by a value function learned from self-play, with the mobility model as the prior, and Monte-Carlo tree search or a policy network to focus the search on the few hundred plausible moves out of \(\approx 320.6\).
  3. Opening and middlegame knowledge. Opening books mined from self-play, and measured strength ratings of each version against the previous one (we already have an AI-versus-AI match harness for this).
  4. Endgame tablebases. Exact retrograde solution of small-material endgames, starting from King + one piece against King (\(4.3\times10^{9}\) states, Section 3.1), then positions with two or three pieces per side. These are strongly solved sub-games, and they give the search exact values at the leaves.
  5. Solved fragments of the rules. Complete solutions of reduced boards (for example \(N=8,\dots,12\) with scaled-down setups) to learn how first-player advantage and drawishness depend on size, which is evidence about the full game.
  6. Verified solvers. Where a computation claims a game-theoretic value (a tablebase, a reduced-board solution) we will certify it with a proof object checked in Lean (Section 9, M8), so a published result is not just “the program said so”.

We expect a full solution of Taikyoku shogi to remain out of reach for a long time, if it is possible at all; the point of the program is to make the AI measurably stronger, to establish exact results on every fragment that can be solved, and to say precisely where the boundary lies. O

11. Open problems

  1. Is there a first-player advantage? (Even for chess and shogi this is unknown; here it is far from decidable by search.) O
  2. What is the empirical distribution of game length under strong play? It fixes the real size of the game tree (Section 4).
  3. Exact reachable-state counts for small material (Section 3.1), and the longest forced win in King + piece vs King for each kind.
  4. A tight combinatorial bound on the number of reachable positions in terms of the multiplicities \(m_k\).
  5. Complexity of the scaled family (Section 8).
  6. Do range-capturing generals admit an elegant potential function proving that long sequences of captures must end (so that no cycle of pure captures exists)? Trivial for captures (the piece count decreases), but the stronger question about bounded numbers of non-capturing moves between captures is open.

References

  1. H. Adachi, H. Kamekawa and S. Iwata. Shogi on \(n\times n\) board is complete in exponential time. Trans. IEICE J70-D(10):1843–1852, 1987 (in Japanese).
  2. L. V. Allis. Searching for Solutions in Games and Artificial Intelligence. PhD thesis, University of Limburg, 1994.
  3. R. Betza. Chess with different armies and the “funny notation” for piece moves. Chess Variant Pages, 1996.
  4. L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. CADE-28, 2021.
  5. A. S. Fraenkel and D. Lichtenstein. Computing a perfect strategy for \(n\times n\) chess requires time exponential in \(n\). J. Combin. Theory Ser. A 31(2):199–214, 1981.
  6. G. Hodges. Ten Shogi Variants. 2002.
  7. J. M. Robson. The complexity of Go. Proc. IFIP Congress, 1983.
  8. C. E. Shannon. Programming a computer for playing chess. Philosophical Magazine 41(314):256–275, 1950.
  9. J. Tromp. Counting legal Go positions (with G. Farnebäck), 2016, and his estimates of the number of chess positions.
  10. “Taikyoku shogi”, English Wikipedia (CC BY-SA 4.0): the source of the piece list and setup used here.

The engine, the data and the script that produced every V number are in the project repository; the numbers on this page are regenerated by python3 tools/build_math.py from data/math_stats.json. Found an error or want to help with the Lean development? hello@taikyokushogi.com.