All missions

Motivation

The irrationality of $\pi$ rules out an exact representation as a rational number. A quantitative question asks how closely rational numbers can approximate it as their denominators grow. The irrationality measure records the threshold exponent for exceptionally accurate rational approximations. This mission formalizes the historical upper-bound milestone $\mu(\pi)\le42$ listed as $C_{7a}$ in the optimization constants project.

Mahler's 1953 paper establishes a stronger, explicit inequality in Theorem 1. The mission extracts its consequence for the irrationality measure and states that consequence through a shared Lean predicate. The number 42 is the chosen historical milestone; it is neither a claim about the exact value of the measure nor a claim to the strongest bound mentioned anywhere in Mahler's paper. Mahler, original p. 33.

Setting

Write $p\in\mathbb Z$ for a numerator and $q\in\mathbb N$ for a positive denominator. The approximation error is the real number $|\pi-p/q|$. The exponent $B$ describes an upper bound on the irrationality measure through an eventual lower bound on this error.

The shared predicate PiIrrationality.UpperBound B means that for every real $\varepsilon>0$, some natural-number threshold $Q$ satisfies

$$\frac{1}{q^{B+\varepsilon}}<\left|\pi-\frac pq\right|$$

for every integer $p$ and every natural number $q>0$ with $Q\le q$. The threshold can depend on $\varepsilon$ and on the chosen bound $B$; it cannot depend on the later choices of $p$ or $q$. Numerators may be negative, zero, or positive. Fractions need not be in lowest terms. This is the epsilon characterization used in the definition of $C_{7a}$.

Formalization targets

The goal is

$$\mu(\pi)\le42,$$

represented by PiIrrationality.UpperBound (42 : ℝ). Expanded, the target is

$$\forall\varepsilon>0\;\exists Q\in\mathbb N\;\forall p\in\mathbb Z\;\forall q\in\mathbb N,\quad q>0\ \land\ Q\le q\ \Longrightarrow\ \frac1{q^{42+\varepsilon}}<\left|\pi-\frac pq\right|.$$

The mission contains one shared definition and one goal theorem. The definition introduces the proposition without asserting any bound. The theorem has no additional hypotheses, and its proof is intentionally left open. Future historical-bound missions can import the same definition and state a different numeric bound without changing the quantity being tracked.

Significance

A finite upper bound restricts the quality of rational approximations to $\pi$ and excludes approximation at arbitrarily large exponents. The formal result would supply a reusable quantitative fact beyond the assertion that $\pi$ is irrational. The published mathematical result is known; the work requested here is a machine-checked proof of the stated consequence.

The shared definition also fixes the meaning of all entries in the accompanying campaign. A smaller bound makes a stronger claim. A proof of a stronger entry may establish this historical goal as a consequence, provided it uses the same definition and no extra hypotheses. The mission remains mathematically valid after further improvements to the numerical bound.

Difficulty

A proof that $\pi$ is irrational only establishes nonzero approximation errors. The target requires a uniform lower estimate over every numerator once the denominator passes a threshold. Checking finitely many rational approximations cannot establish the quantified conclusion. A formal development must control the dependence of its estimates and thresholds, and justify every passage between an analytic estimate and the final rational-approximation inequality.

The exact theorem from Mahler should be distinguished from this goal: his explicit uniform inequality is stronger than the eventual epsilon statement recorded here. A proof may pass through that uniform result, but the goal does not require a particular proof method, a particular threshold, or a separate treatment of every auxiliary theorem in the original paper.

Formalization scope

The circle constant is Mathlib's Real.pi. Absolute value, division, and exponentiation in the displayed inequality are operations on the real numbers; in particular, $q^{42+\varepsilon}$ is a real power. The denominator is explicitly positive, so division by zero cannot satisfy the premises. Allowing $Q=0$ does not remove the positivity requirement on $q$.

The definition is stored in Definitions.Def_PiIrrationality_UpperBound. The goal imports this definition instead of introducing another version of it. The conclusion is not placed among the theorem's assumptions. The definition contains no proof placeholder; the sole sorry is the open proof of the goal theorem. Contributions may establish supporting estimates or a complete proof while preserving these conventions.

Selected references

• K. Mahler, On the approximation of π, Nederl. Akad. Wetensch. Proc. Ser. A 56 = Indag. Math. 15 (1953), 30–42, Theorem 1, p. 33. EMS reprint.
• Optimization problems project, The irrationality measure of π, constant $C_{7a}$: definition and historical bounds. Source page.

Motivation

Chess, checkers, Go and Backgammon share a feature that card games such as Poker lack: whenever a player moves, the player knows everything that has happened so far. von Neumann and Morgenstern call this perfect information and devote §15 of Theory of Games and Economic Behavior (1944; 3rd ed. 1953) to it. Their result is that such a game, viewed as a zero-sum two-person game, is strictly determined: it has a value that each player can secure with a pure strategy, without any randomization. For Chess this means that exactly one of three statements is true: White can force a win, Black can force a win, or both can force at least a draw ((15:D:a)–(15:D:c)).

Timeline. Zermelo (1913, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels) showed for Chess that either one side can force a win or both can avoid losing; his argument is not phrased in terms of strategies and a value, and was later corrected and completed by König (1927) and Kalmár (1928/29). von Neumann and Morgenstern (1944, §15) proved strict determinateness for every finite zero-sum two-person game with perfect information, including chance moves (15.7.1), and gave the explicit formula (15:12) for the value. Kuhn (1953, Extensive games and the problem of information, Annals of Mathematics Studies 28) recast games in tree form and extended the pure-strategy existence result to general-sum games with perfect information (subgame-perfect equilibria by backward induction).

Setting

A game tree $\Gamma$ is a finite rooted tree. Each leaf is a finished play $\pi$ and carries the payoff $\mathfrak F_1(\pi) \in \mathbb R$ to player 1; player 2 receives $-\mathfrak F_1(\pi)$. Each internal node is a move $\mathfrak M$ of one of three kinds $k$, with alternatives $\sigma = 1, \dots, \alpha$ leading to subtrees $\Gamma_\sigma$:

• $k = 0$, a chance move, where alternative $\sigma$ occurs with probability $p(\sigma) \geqq 0$, $\sum_\sigma p(\sigma) = 1$;
• $k = 1$, a personal move of player 1, with $\alpha \geqq 1$;
• $k = 2$, a personal move of player 2, with $\alpha \geqq 1$.

A pure strategy $\tau_1$ of player 1 is a complete plan choosing an alternative at every node of kind 1; $\tau_2$ does the same at every node of kind 2. The normalized form $\mathcal H(\tau_1, \tau_2)$ is the expected payoff to player 1, the expectation being over the chance moves. With the maxima and minima taken over the finitely many pure strategies,

$$v_1 = \operatorname{Max}_{\tau_1} \operatorname{Min}_{\tau_2} \mathcal H(\tau_1, \tau_2), \qquad v_2 = \operatorname{Min}_{\tau_2} \operatorname{Max}_{\tau_1} \mathcal H(\tau_1, \tau_2).$$

Always $v_1 \leqq v_2$; the game is strictly determined when $v_1 = v_2$ (14.4.2).

For a function $f(\sigma_1)$ of the alternatives of the first move $\mathfrak M_1$, of kind $k_1$, the operation $M^{k_1}_{\sigma_1}$ of (15:8) is $\sum_{\sigma_1} p_1(\sigma_1) f(\sigma_1)$, $\operatorname{Max}_{\sigma_1} f(\sigma_1)$ or $\operatorname{Min}_{\sigma_1} f(\sigma_1)$ for $k_1 = 0, 1, 2$. Applying these operations from the leaves back to the root gives the backward-induction value $v(\Gamma)$.

Formalization targets

Goal: 15.6.1 with (15:12)

For every finite game tree $\Gamma$,

$$v_1 = v_2 = v = M^{k_1}_{\sigma_1} M^{k_2(\sigma_1)}_{\sigma_2} \cdots M^{k_\nu(\sigma_1, \dots, \sigma_{\nu-1})}_{\sigma_\nu} \mathfrak F_1(\pi(\sigma_1, \dots, \sigma_\nu)).$$

Both the equality $v_1 = v_2$ and the value formula are part of the goal.

Milestones

• (13:E): for finite nonempty domains and $f$ ranging over all functions of $x$, $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Min}_f \operatorname{Max}_x \psi(x, f(x))$; and (13:G): $\operatorname{Max}_x \operatorname{Min}_f \psi(x, f(x)) = \operatorname{Max}_x \operatorname{Min}_u \psi(x, u)$.
• (15:2)–(15:7): $v_k = M^{k_1}_{\sigma_1} v_{\sigma_1/k}$ for $k = 1, 2$, one milestone for each kind of first move, without assuming that any game is strictly determined.
• (15:C:a): a game of length $0$ is strictly determined with value $w$; (15:C:b): if every $\Gamma_{\sigma_1}$ is strictly determined, so is $\Gamma$.
• (15:13), (15:D:a)–(15:D:c): for games without chance moves whose plays end in $1, 0, -1$, the value is one of these three numbers, and it decides which player can force a win or whether both can force a tie.

Significance

The theorem is the first existence result for the value of a class of games in pure strategies. It shows that the whole difficulty of the general zero-sum two-person game, the need for mixed strategies (§17), comes from imperfect information. It gives a construction as well as an existence proof: the value and optimal strategies are computed by backward induction, the procedure behind retrograde analysis of endgames, minimax search in game-playing programs, and the dynamic programming recursions of sequential decision problems with an adversary. The Chess trichotomy (15:D) is its best-known consequence.

Formalizing it adds a checked account of the passage from the extensive to the normalized form for a whole class of games, which the book carries out informally (15.4.2, 15.5.1: "the reader may verify it from the formalistic point of view"). The result is classical and fully proved in the book; the work is to formalize that proof on a tree model. Mathlib has saddle points (Order/SaddlePoint) and the minimax theorem for continuous functions (Topology/Sion), but no game trees, strategies of extensive games, or backward induction. No machine-checked version of this theorem with chance moves and the normalized form over complete plans is known to the mission.

Difficulty

The recursions (15:2)–(15:7) are not formal consequences of the definitions: $v_1$ and $v_2$ are extrema over whole plans of $\Gamma$, while the right-hand sides are extrema over plans of the separate games $\Gamma_{\sigma_1}$. At a personal move of player 1, $v_2 = \operatorname{Max}_{\sigma_1} v_{\sigma_1/2}$ requires interchanging a Min over player 2's plans, which are functions of player 1's first choice, with a Max over that choice: this is exactly (13:E), a max-min equality that fails for general functions of two variables and holds here because the minimizing variable is a function of the maximizing one. A proof that treats the Max over $\tau_1$ and the Min over $\tau_2$ as interchangeable without this step is circular.

A second difficulty is the strategy spaces themselves. A complete plan chooses at nodes the plan itself excludes, so the pure strategies of $\Gamma$ are not simply pairs of a first choice and one strategy of the chosen subgame; the identification the book uses in 15.5.1 has to be justified by showing that the extra coordinates do not change $\mathcal H$.

Formalization scope

A game is an inductive type GameTree with constructors leaf w, chance α p next hp hsum, move1 α hα next, move2 α hα next; alternatives are Fin α (numbered from $0$). The conditions $p \geqq 0$, $\sum p = 1$ and $\alpha \geqq 1$ at personal moves are constructor fields, so every tree is a legitimate game. Pure strategies are dependent types Strategy1 t, Strategy2 t defined by recursion on the tree (complete plans), with Fintype and Nonempty instances; $\mathcal H$ is payoff t τ₁ τ₂, the expected leaf payoff; v1, v2 are Finset.sup'/Finset.inf' over all strategies, so every Max and Min is attained.

Standing hypotheses and conventions taken from the book:

• finite strategy sets and attained extrema (13.2.1, 14.1.1): finite trees with finitely many alternatives at every move;
• perfect information, i.e. preliminarity equals anteriority (6.4.1, (15:B)): built into the tree model, which is the sequence of games (15:1);
• zero-sum two-person (15.3.1): one payoff $\mathfrak F_1$, player 2 receives $-\mathfrak F_1$ and minimizes $\mathcal H$;
• chance probabilities nonnegative and summing to one (15.4.2, 10.1.1); $\alpha \geqq 1$ at every move;
• (15:D) additionally assumes no chance moves and outcomes $1, 0, -1$ (15.7.1).

The book's formal model is the set-theoretic one of §§9–10, with partitions of the set of plays; the tree restates it for the perfect-information case and does not formalize §§9–10. The book fixes one length $\nu$ for all plays; trees with plays of different lengths contain the book's games as a special case, so the goal is at least as strong as the book's theorem.

Strategies are plans, never responses: a strategy of player 1 is fixed before play and cannot depend on player 2's strategy, which would make $v_1 = v_2$ trivial. Chance moves are part of the goal; a version without them proves only the Chess case and is weaker than the book.

Reusable beyond this mission: the tree model, its strategy types and the normalized form, which later chapters on extensive games can import. Welcome contributions: proofs of the milestones, and a lemma identifying the strategies of $\Gamma$ with the book's recursive description (15.4.2, 15.5.1).

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§6, 11, 13–15. https://doi.org/10.1515/9781400829460
• E. Zermelo, Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels, Proc. Fifth International Congress of Mathematicians, vol. II, 1913, pp. 501–504.
• U. Schwalbe, P. Walker, Zermelo and the early history of game theory, Games and Economic Behavior 34 (2001), 123–137. https://doi.org/10.1006/game.2000.0794
• H. W. Kuhn, Extensive games and the problem of information, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton, 1953, 193–216. https://doi.org/10.1515/9781400881970-012

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$, and $J$ is the finite set of bases. For each base $j$:

• $T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$;
• $T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$, integers with $1 \le T^e_{ij} < T^r_{ij}$;
• $\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$. The latter is constant for $t \ge T^r_{ij}$, since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
• $X_{ijt}$ is the cumulative demand at base $j$ through period $t$, a nonnegative integer random variable, nondecreasing in $t$, with finite mean;
• $h_{ij} > 0$, $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$, the expected cost of that period is

$$G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,$$

and stock left at the end of the horizon costs

$$Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .$$

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$, $t = 0, \dots, T_{i0}$, with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$, and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$. The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$, which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$. Its largest optimal solution is written $\hat S_{ijt}$.

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$, for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$,

$$\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.$$

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

1. Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$: its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$.
2. Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$.
3. The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$.
4. Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$.
5. Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$, $\tilde S_{ijt} \le S^*_{ijt}$. Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$, also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$, provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$.

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$. Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$, an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$. This must be shown feasible, to change only $S_{ijk}$, and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$, and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

• One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$, [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
• $G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$, and a tsum for $Q$. The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$.
• "The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
• "An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
• Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$'s series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$", the book's $\lceil F^{-1}\rceil$/$\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso "$T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$". Separability is stated both for optimal plans and for optimal values.
• Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
• Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
• The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$. Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
• K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

Motivation

Some elementary functions, such as $e^{-x^2}$, $\sin(x)/x$ and $x^x$, have antiderivatives that cannot be written as elementary functions. Liouville's theorem, formulated by Joseph Liouville between 1833 and 1841, is the algebraic statement that explains when an elementary antiderivative can exist: if a function has an elementary antiderivative at all, then that antiderivative lies in the differential field of the function, plus finitely many logarithms. The theorem underlies the Risch algorithm for symbolic integration, which relies on it to find any elementary antiderivative.

Setting

A differential field is a field $F$ together with a derivation $D : F \to F$, i.e. an additive map satisfying $D(ab) = a\,Db + b\,Da$. Its constants form the subfield

$$\operatorname{Con}(F) = \{ f \in F : Df = 0 \}.$$

Let $G \supseteq F$ be a differential field extension (the derivation of $G$ restricts to that of $F$).

• $G$ is a logarithmic extension of $F$ if $G = F(t)$ with $t$ transcendental over $F$ and $Dt = Ds/s$ for some nonzero $s \in F$ (so $t$ behaves like $\log s$).
• $G$ is an exponential extension of $F$ if $G = F(t)$ with $t$ transcendental over $F$ and $Dt/t = Ds$ for some $s \in F$ (so $t$ behaves like $e^{s}$).
• $G$ is an elementary differential extension of $F$ if there is a finite chain of subfields $F = K_0 \subseteq K_1 \subseteq \cdots \subseteq K_m = G$ in which every step $K_{i+1} = K_i(t_i)$ is algebraic, logarithmic or exponential.

The running example is $\mathbb{C}(x)$, the field of rational functions in one variable with the standard derivative $d/dx$.

Formalization targets

Goal: Liouville's theorem

Let $F \subseteq G$ be differential fields of characteristic zero with $\operatorname{Con}(F) = \operatorname{Con}(G)$, and let $G$ be an elementary differential extension of $F$. If $f \in F$ and $g \in G$ satisfy $Dg = f$, then there are $n \ge 0$, constants $c_1, \dots, c_n \in \operatorname{Con}(F)$ and nonzero $f_1, \dots, f_n \in F$, and $s \in F$ with

$$f = c_1 \frac{Df_1}{f_1} + \cdots + c_n \frac{Df_n}{f_n} + Ds.$$

Milestones from the article

1. The constants $\operatorname{Con}(F)$ form a subfield of $F$.
2. $\mathbb{C}(x)$ carries a (unique) derivation extending the formal derivative of polynomials.
3. $\operatorname{Con}(\mathbb{C}(x)) = \mathbb{C}$.
4. $1/x$ has no antiderivative in $\mathbb{C}(x)$.
5. The antiderivatives $\ln x + C$ of $1/x$ exist in the logarithmic extension $\mathbb{C}(x, \ln x)$.
6. $1/(x^2+1)$ has no antiderivative in $\mathbb{C}(x)$.
7. $\displaystyle \frac{1}{x^2+1} = \frac{1}{2i}\,\frac{Du}{u}$ with $u = \frac{1+ix}{1-ix}$, i.e. $\tan^{-1} x = \frac{1}{2i}\ln\frac{1+ix}{1-ix}$ has the form required by the theorem.

Significance

The theorem reduces the question of whether an integral is elementary to a question about the base differential field. That reduction is what makes decision procedures for integration in finite terms (the Risch algorithm) possible, and it is the standard route to proving that $e^{-x^2}$, $\sin(x)/x$ or $x^x$ have no elementary antiderivative.

The result is classical and proved (Liouville; modern algebraic proof by Rosenlicht; textbook proof in Geddes–Czapor–Labahn, §12.4). Mathlib contains a formalization of the algebraic-extension part of the argument (IsLiouville, isLiouville_of_finiteDimensional in Mathlib/FieldTheory/Differential/Liouville.lean); the logarithmic and exponential steps and the full theorem for elementary extensions are the remaining work.

Difficulty

The algebraic steps can be handled by taking traces. The central difficulty is the transcendental steps: for a logarithmic or exponential generator $t$ one must show, by comparing partial-fraction expansions in $t$ and degrees in $t$, that an expression of the Liouville form over $K(t)$ can be pushed down to one over $K$. This needs the hypothesis that no new constants appear. The induction must also track how constants and logarithmic derivatives behave along the whole chain.

Formalization scope

A differential field is a Mathlib Field with a Differential instance (a derivation over $\mathbb{Z}$, written $a'$); the extension $F \subseteq G$ is an Algebra F G with DifferentialAlgebra F G, i.e. $D$ commutes with the embedding. The chain of the elementary extension is a sequence of IntermediateField F G, starting at $\bot$ and ending at $\top$. Each step adjoins a single element, which is algebraic, logarithmic, or exponential over the previous field, and every derivative is computed in $G$. Characteristic zero is assumed (CharZero F). The article does not state it, but it is the standing convention of the theorem in its standard sources. $\operatorname{Con}(F) = \operatorname{Con}(G)$ is stated as the equality of the image of $\operatorname{Con}(F)$ with $\operatorname{Con}(G)$. In the conclusion, the $f_i$ are required to be nonzero, so the quotients $Df_i/f_i$ carry no division-by-zero junk.

For the $\mathbb{C}(x)$ examples, $\mathbb{C}(x)$ is Mathlib's RatFunc ℂ. Mathlib does not provide its derivative, so the examples take an arbitrary derivation satisfying IsStandardDerivation (it agrees with the formal derivative on polynomials). Milestone 2 asserts that exactly one such derivation exists, so the examples are not vacuous.

Selected references

• J. Liouville, Premier / Second mémoire sur la détermination des intégrales dont la valeur est algébrique, J. École Polytechnique XIV (1833), 124–193.
• M. Rosenlicht, Integration in finite terms, Amer. Math. Monthly 79 (1972), 963–972. https://doi.org/10.2307/2318066
• K. O. Geddes, S. R. Czapor, G. Labahn, Algorithms for Computer Algebra, Kluwer, 1992, §12.4.
• Wikipedia, Liouville's theorem (differential algebra), oldid 1349223559.

Motivation

Given a monic polynomial $f$ with integer coefficients, one can reduce it modulo each prime $p$ and factor it over the finite field $\mathbb F_p$. The way $f$ factors changes with $p$, and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over $\mathbb Q$ with a minimum of terminology.

Timeline.

• 1837 — Dirichlet: primes are equidistributed (in analytic density) over the invertible residue classes modulo $m$.
• 1880/1896 — Frobenius: the density of primes with a given decomposition type of $f$ modulo $p$ equals the proportion of Galois group elements with that cycle pattern; he conjectures the sharper statement for conjugacy classes.
• 1896 — de la Vallée-Poussin: Dirichlet's theorem for natural density.
• 1922/1925 — Chebotarëv proves Frobenius's conjecture, without class field theory.
• 1935 — Deuring's proof via Artin reciprocity, now the textbook route.

Setting

Let $f\in\mathbb Z[X]$ be monic of degree $n$ with nonzero discriminant $\Delta(f)$, so that $f$ has $n$ distinct complex zeros $\alpha_1,\dots,\alpha_n$. Let $K=\mathbb Q(\alpha_1,\dots,\alpha_n)$ be its splitting field and $G=\mathrm{Gal}(K/\mathbb Q)$ its Galois group. Every $\sigma\in G$ permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of $\sigma$, a partition of $n$.

For a prime $p\nmid\Delta(f)$, the degrees of the irreducible factors of $f \bmod p$ over $\mathbb F_p$ form the decomposition type of $f$ modulo $p$, again a partition of $n$.

A Frobenius substitution of $p$ is an element $\sigma\in G$ such that, for some prime ideal $\mathfrak Q$ of the ring of integers $\mathcal O_K$ lying over $p$,

$$\sigma(x)\equiv x^p \pmod{\mathfrak Q}\qquad\text{for all }x\in\mathcal O_K .$$

For $p\nmid\Delta(f)$ these elements form a single conjugacy class of $G$, written $\sigma_p$.

A set $S$ of primes has (analytic, or Dirichlet) density $\delta$ if

$$\frac{\sum_{p\in S}p^{-s}}{\log\frac{1}{s-1}}\longrightarrow\delta\qquad(s\downarrow 1),$$

and natural density $\delta$ if $\#\{p\le x:p\in S\}/\#\{p\le x\}\to\delta$ as $x\to\infty$.

Formalization targets

Goal: Chebotarëv's density theorem

For every conjugacy class $C$ of $G$,

$$\text{the set }\{p \text{ prime}: p\nmid\Delta(f),\ \sigma_p\in C\}\text{ has analytic density }\frac{\#C}{\#G}.$$

Milestones

1. Theorem of Dirichlet: for $m\ge1$ and $\gcd(a,m)=1$, the primes $p\equiv a \pmod m$ have density $1/\varphi(m)$.
2. A set of primes with natural density $\delta$ has analytic density $\delta$.
3. Galois theory of finite fields: for a squarefree $g\in\mathbb F_p[X]$, the cycle pattern of $x\mapsto x^p$ on the zeros of $g$ equals the decomposition type of $g$.
4. For $p\nmid\Delta(f)$, the Frobenius substitutions of $p$ form exactly one conjugacy class of $G$.
5. For $p\nmid\Delta(f)$, the cycle pattern of $\sigma_p$ equals the decomposition type of $f$ modulo $p$.
6. For $f=X^m-1$ and $p\nmid m$, $\sigma_p(\zeta)=\zeta^p$ for every primitive $m$-th root of unity $\zeta$; that is, $\sigma_p$ corresponds to $p \bmod m$ under $G\cong(\mathbb Z/m\mathbb Z)^\times$.
7. Theorem of Frobenius: the primes $p\nmid\Delta(f)$ for which $f$ has a given decomposition type $t$ have density $\#\{\sigma\in G:\text{cycle pattern }t\}/\#G$.

Significance

Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if $f$ has a zero modulo almost every prime then $f$ is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on $\ell$-adic representations).

The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.

Difficulty

The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in $\mathcal O_K$ with factorization of $f$ modulo $p$, including the fact that $p\nmid\Delta(f)$ forces $p$ to be unramified in $K$. The analytic core is harder: one needs Dedekind zeta functions and $L$-functions of number fields and their behaviour at $s=1$. The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over $\mathbb Q$; in particular, the statement over $\mathbb Q$ alone cannot be proved by induction on itself.

Formalization scope

All declarations live in the namespace ChebotarevDensity and share one definition file.

• $K$ is Mathlib's SplittingField of $f$ viewed in $\mathbb Q[X]$; $G$ is Polynomial.Gal; $\Delta(f)$ is Mathlib's Polynomial.discr.
• A Frobenius substitution is expressed with Mathlib's IsArithFrobAt at some prime ideal of $\mathcal O_K$ containing $p$; "$\sigma_p\in C$" means that some Frobenius substitution of $p$ lies in $C$ (for $p\nmid\Delta(f)$ this is equivalent to all of them lying in $C$, by milestone 4).
• The cycle pattern is Equiv.Perm.partition of the permutation induced on the complex zeros of $f$; it includes fixed points.
• The decomposition type is the multiset of degrees of the normalized (monic) irreducible factors of $f \bmod p$.
• Analytic density uses $\sum' p^{-s}$ over the primes of $S$ and the limit $s\to1^+$ within $(1,\infty)$; natural density compares prime counts up to $x\in\mathbb N$.
• The hypotheses $\Delta(f)\neq0$ and "$f$ monic" are those of the source; the theorems are not vacuous, since e.g. $f=X^m-1$ satisfies them.

Welcome contributions: Dedekind zeta functions and Hecke $L$-functions at $s=1$, the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.

Selected references

• P. Stevenhagen, H. W. Lenstra, Jr., Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, 26–37. doi:10.1007/BF03027290
• N. Tschebotareff, Die Bestimmung der Dichtigkeit einer Menge von Primzahlen, welche zu einer gegebenen Substitutionsklasse gehören, Math. Ann. 95 (1925), 191–228. doi:10.1007/BF01206606
• S. Lang, Algebraic Number Theory, Addison-Wesley, 1970, Chap. VIII.
• J. Neukirch, Class Field Theory, Springer, 1986, Chap. V.
• Chebotarev density theorem, Wikipedia. link

Motivation

In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).

This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.

Setting

A cognitive-consequence space is a set $C$ of mental representations (thoughts) with a consequence operator $\mathrm{Cn} : \mathcal P(C) \to \mathcal P(C)$ and an implication connective $X \Rightarrow Y$ satisfying Tarski's axioms as listed in the paper (p. 5):

1. $C$ is countable;
2. $A \subseteq \mathrm{Cn}(A)$;
3. $A \subseteq B \Rightarrow \mathrm{Cn}(A) \subseteq \mathrm{Cn}(B)$;
4. $\mathrm{Cn}(\mathrm{Cn}(A)) = \mathrm{Cn}(A)$;
5. if $X \in \mathrm{Cn}(A)$ then $X \in \mathrm{Cn}(B)$ for some finite $B \subseteq A$;
6. if $Y \in \mathrm{Cn}(A \cup \{X\})$ then $(X \Rightarrow Y) \in \mathrm{Cn}(A)$;

together with the paper's standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$ (p. 5, after Definition 3.2).

A set $A$ is deductive if $\mathrm{Cn}(A) = A$. The cognitive-consequence topology is

$$\tau = \{A \subseteq C : \mathrm{Cn}(C \setminus A) = C \setminus A\},$$

and members of $\tau$ are consequence-wise open (CWO). The cognitive closure $\mathrm{Cl}^{\square}(A)$ is the intersection of all deductive sets containing $A$.

Separately, a cognitive similarity distance is a function $\mathrm{Cog} : C \times C \to [0,1]$ together with a relation $x \approx y$ ("$x$ and $y$ cognitively coincide") such that $\mathrm{Cog}(x,y) = 0 \iff x \approx y$, $\mathrm{Cog}$ is symmetric, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality holds. A sequence of thoughts $(x_n)$ converges to $x$ if for every $\varepsilon \in (0,1)$ we have $\mathrm{Cog}(x, x_n) < \varepsilon$ for all large $n$.

Formalization targets

Goal: "human intelligence is limitless" (Theorems 3.3 and 3.4)

For every cognitive-consequence space,

$$\Bigl(\exists f \in C\ \forall A \in \tau,\ f \notin A\Bigr) \ \wedge\ \Bigl(\exists f \in C\ \exists A \in \tau,\ f \in A\Bigr).$$

Milestones

Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology $\tau$ and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter $f_d$) and Theorem 5.1 (Gödel's incompleteness black hole).

Significance

The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about $\tau$, cognitive closure and cognitive limits.

Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$. The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with $\mathrm{Cn}(A) = C$ for every $A$, on a one-point language, satisfies all of them and has $\tau = \{\varnothing\}$. The goal is therefore expected to be resolved by a disproof.

Difficulty

The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from $C$ (a consistent theory). The paper's argument for Theorem 3.4 derives $\bigcap_i A_i = \varnothing$ and calls this a contradiction; nothing in the axioms forbids it.

Formalization scope

• CogCons.CognitiveConsequenceSpace C bundles $\mathrm{Cn}$, the connective imp, axioms (i)–(vi) and $\mathrm{Cn}(\varnothing) \neq \varnothing$. The syntax $\sigma$ and interpretation $I$ of the paper are not modelled beyond imp.
• The paper also asserts $\mathrm{Cn}(C) \neq C$ (p. 5). This contradicts axiom (ii), since $C \subseteq \mathrm{Cn}(C) \subseteq C$; including it would make every statement vacuously true, so it is omitted. For the same reason the second half of Corollary 3.4 ($\mathrm{Cl}^{\square}(C) \neq C$) is not included.
• Theorem 4.4 (the family $\{A : f \in \mathrm{Cn}(A)\}$ is a filter) is not included: closure under intersection fails in a four-element model satisfying all the axioms.
• Results relying on informal notions (the practical topology of Section 2, Theorems 3.9–3.11 and 3.13, Theorems 4.1–4.2, and the "solution space" of Section 5) are not formalized.
• CogCons.CognitiveSimilarityDistance C is independent of $\mathrm{Cn}$; sequences are indexed by $\mathbb N$ starting at $0$; $\approx$ is an arbitrary relation constrained only by the listed axioms.

Selected references

• S. Acharjee, U. Gogoi, The limit of human intelligence, arXiv:2310.10792v2 [math.GM], 2023. https://arxiv.org/abs/2310.10792
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20(2), 7–15, 1998. https://doi.org/10.1007/BF03025291