Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.
Theorem selected for verification:OAI.binary_sweep_contraction_and_mixing
The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.
theorembinary_sweep_contraction_and_mixing : BinaryCoordinateSweeps.BinaryContractionTarget ∧ (∀ d : ℕ, 0 < d → ∑ g : Equiv.Perm (BinaryCoordinateSweeps.Slot d), BinaryCoordinateSweeps.binaryLaw d g * BinaryCoordinateSweeps.realSign g = 0) ∧ BinaryCoordinateSweeps.UniformSweepMixingTarget := bysorry
A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.
Definitions needed to read it
Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.
defcoordinateLayer (d : ℕ) (j : Fin d) (c : (({i : Fin d // i ≠ j} → Bool)) → Bool) : Equiv.Perm (Slot d) :=let e := Equiv.piSplitAt j (fun _ : Fin d => Bool)let sw : Equiv.Perm (Bool × ({i : Fin d // i ≠ j} → Bool)) := { toFun := fun x => (x.1 ^^ c x.2, x.2) invFun := fun x => (x.1 ^^ c x.2, x.2) left_inv := fun x => by simp right_inv := fun x => by simp } e.trans (sw.trans e.symm)
defUniformSweepMixingTarget : Prop := ∃ w : ℕ, ∀ ε : ℝ, 0 < ε → ∃ d₀ : ℕ, ∀ d ≥ d₀, ∀ τ : Equiv.Perm (Slot d), totalVariation (fun g => sweepLaw d w (g * τ⁻¹)) (uniformLaw (Equiv.Perm (Slot d))) ≤ ε
Possible paper match, with no recorded review
Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.
Words of the Lean statement, its names split into words, that also appear in the theorem: binary, contraction, initial, sign, representation, decks, independent, deterministic and eight more. Found in the paper’s title, which its main theorem states: coordinate.
Theorem 1.1 of Conditional coordinate sweeps and analytic transfer
Theorem(Binary sweep contraction)
There are absolute constants g>0 and d_0 such that, for d\ge d_0 and every \lambda\vdash 2^d,
\|K_\lambda\|_{\op}\le D_\lambda^{-g}.
The sign representation is annihilated. There is an absolute positive integer w such that the law after w independent sweeps converges to uniform in total variation as d\to\infty, uniformly over deterministic initial decks.
There are absolute constants \(g>0\) and \(d_0\) such that, for \(d\ge d_0\)
and every \(\lambda\vdash 2^d\),
\[
\|K_\lambda\|_{\op}\le D_\lambda^{-g}.
\]
The sign representation is annihilated. There is an absolute positive integer \(w\)
such that the law after \(w\) independent sweeps converges to uniform in
total variation as \(d\to\infty\), uniformly over deterministic initial
decks.
Other possible paper matches, closest wording first
Theorem 1.1 of Conditional permutations in a revealed switching environment. Words of the Lean statement, its names split into words, that also appear in the theorem: slot, mixing, initial, deck, deterministic, uniformly and five more. Found in the paper’s title, which its main theorem states: switching. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: approaches.
Theorem 16.1 of Random coordinate frames and partial permutation laws. Words of the Lean statement, its names split into words, that also appear in the theorem: half, layers, positions, coordinate, list, deck and seven more. Found in the paper’s title, which its main theorem states: laws. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: zero.
Theorem 10.1 of Conditional information under deterministic coordinate sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: switches, real, contraction, mass, signed, coordinate and five more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sufficiently and large.
Theorem 15.1 of Random coordinate frames and partial permutation laws. Words of the Lean statement, its names split into words, that also appear in the theorem: switches, mix, initial, deck, independent, one and three more. Found in the paper’s title, which its main theorem states: coordinate and laws. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: zero, sufficiently and large.
Theorem 5.3 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: layer, number, dimension, contraction, irreducible, total and three more. Found in the paper’s title, which its main theorem states: representation. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: zero, sufficiently and large.
Theorem 12.2 of Conditional information under deterministic coordinate sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: identities, natural, independent, law, integer, uniform and one more. Found in the paper’s title, which its main theorem states: coordinate, deterministic and sweeps.
How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.
Reported Comparator runs
two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.
For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…
AcceptedTheir term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
AcceptedTheir term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.
This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.
Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.
Do family 238’s Lean statements express the advertised result?
These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
Finds the whole advertised result stated or impliedTheir term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: ThorpResults.remaining_main (ThorpRemaining) is a conjunction whose last conjunct OptimalOrderMain := IsTheta atTop (mixingTime d) (log (2^d)) states exactly the Θ(log N) mixing for N = 2^d cards, with mixingTime d := sInf {t | distance d t ≤ 1/4}, distance d t := tv (law d t) (uniform d) the total-variation distance of the full permutation law (and InformationMain records that lawFrom from any starting deck has the same distance, plus distance d (2048 d) → 0); the 12 other challenge files are supporting Fourier/representation estimates (regular_trace_smoothing, binary_sweep_contraction_and_mixing, robust_permanent, ...). All of them state estimates for the same hand-built Thorp shuffle.
Definitions the group asks readers to compare with the paper: Custom Thorp shuffle and 'mixing time': step (d+1) c := (pairSwitch d c on the head bit, then rotate the coordinate order) on State d := Equiv.Perm (Fin d → Bool) with Coins (d+1) = (Fin d → Bool) → Bool iid fair coins, fairMass, tv, mixingTime d := sInf {t | distance d t ≤ 1/4}; this is the standard pair-swap-and-interleave Thorp shuffle and TV-from-uniform with ε = 1/4, but it is a hand-written model and the Θ-statement hides explicit constants (1600d, 2048d, ...). OccupiedOverlap shows an axiom_files hit (HookModel.lean) that is a doc-comment false positive.
OpenAI’s own note on what this Lean statement covers
“The formalized binary-sweep theorem gives a universal power contraction in every irreducible representation: for sufficiently large $d$, the averaged sweep on $2^d$ slots has operator norm at most $D^{-g}$ in representation dimension $D$, for some $g>0$. The sign expectation is zero, and a fixed number of independent sweeps approaches uniform in total variation from every initial deck.”
An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.
Supporting material
The complete Lean statement file
102 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.
Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.
Links in the file: 32 to its own declarations, 49 to Mathlib’s documentation. 19 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.
As $d\to\infty$,
\[
\|q_d^{*(1600d)}-U_n\|_{\mathrm{TV}}\longrightarrow0.
\]
For every integer $t\ge0$,
\[
\|q_d^{*t}-U_n\|_{\mathrm{TV}}
\ge 1-\frac{2^{tn/2}}{n!}.
\]
Consequently the mixing time at distance $1/4$ satisfies
\[
t_{\mathrm{mix}}(d)\ge
\left\lceil\frac2n\log_2\frac{3n!}{4}\right\rceil
=2d-O(1),
\qquad t_{\mathrm{mix}}(d)=\Theta(d).
\]
Theorem(Complementary cosets control Fourier matrices)
Partition X into b nonempty sets M_1,\ldots,M_b. Put H_i=H_{M_i}. Suppose f is a nonnegative measure on G of mass at most one and, for every g\in G and i,
f(gH_i)\le \frac{B}{[G:H_i]}.
For every u>0 and every irreducible \rho of degree D,
Partition $X$ into $b$ nonempty sets $M_1,\ldots,M_b$. Put $H_i=H_{M_i}$. Suppose $f$ is a nonnegative measure on $G$ of mass at most one and, for every $g\in G$ and $i$,
\begin{equation}
f(gH_i)\le \frac{B}{[G:H_i]}.
\end{equation}
For every $u>0$ and every irreducible $\rho$ of degree $D$,
\begin{equation}
\|\widehat f(\rho)\|_{\HS}^2
\le bBC_uD^{-1+(u+2)/b}.
\end{equation}
There is also an independent orbit-span proof of the bound
\begin{equation}
\|\widehat f(\rho)\|_{\op}^2
\le bBC_uD^{-1+(u+2)/b}.
\end{equation}
No restriction is imposed on block sizes or on the multiplicities in $\rho|_{H_1\times\cdots\times H_b}$.
Theorem(Conditional permutation and full-deck mixing)
Let n=2^d, and start the shuffle from any deterministic deck. After J(s_0+1) sweeps, where s_0=400 and J=40000, the conditional free-slot law defined above satisfies
Consequently the full-deck law approaches uniform, uniformly in the starting deck, after 16\,040\,400d physical shuffles. For every integer t\ge0, after t physical shuffles the full-deck distance from uniform is at least 1-2^{tn/2}/n!. Thus the full-deck mixing time is of order d.
Let $n=2^d$, and start the shuffle from any deterministic deck.
After $J(s_0+1)$ sweeps, where $s_0=400$ and $J=40000$, the conditional free-slot law defined above satisfies
\[
\sup_{\text{initial layouts}}\E_{\mathcal E}
\|\nu_{\mathcal E}-U_{n/2}\|_{\TV}\longrightarrow0
\qquad(d\longrightarrow\infty).
\]
Consequently the full-deck law approaches uniform, uniformly in the starting deck, after $16\,040\,400d$ physical shuffles. For every integer $t\ge0$, after $t$ physical shuffles the full-deck distance from uniform is at least
$1-2^{tn/2}/n!$. Thus the full-deck mixing time is of order $d$.
There are absolute constants $\eta,c,C>0$ such that, with $a=1/1000$,
\[
\log\E_{y\sim u_{N,k}}R_x(y)^{1+a}
\le Ck(k/N)^\eta
\qquad(1\le k\le N),
\]
uniformly over every starting injection $x$. For every sufficiently
large dyadic $N$ and every nontrivial irreducible representation,
\[
T_N(\lambda)=0\quad\hbox{or}\quad
\|T_N(\lambda)\|_{\op}\le D_\lambda^{-c}.
\]
Consequently an absolute number of forward sweeps has worst-start
total-variation distance from uniform tending to zero as $d\to\infty$.
There are positive weights W_\lambda, an absolute finite p_*, and real exponents 2\le p_d\le p_* such that, for every d\ge1 and every \lambda\vdash2^d,
There are positive weights $W_\lambda$, an absolute finite $p_*$, and real
exponents $2\le p_d\le p_*$ such that, for every $d\ge1$ and every
$\lambda\vdash2^d$,
\begin{equation}
D_\lambda^{3/4}\le W_\lambda\le D_\lambda,
\qquad W_\lambda\|K_d(\lambda)\|_{p_d}^{p_d}\le1.
\end{equation}
Consequently $\|K_d(\lambda)\|_{\rm op}\le D_\lambda^{-3/(4p_*)}$.
Corollary(Optimal order of mixing)
There is an absolute constant C such that, for every d\ge1,
There is an absolute constant $C$ such that, for every $d\ge1$,
\[
\left\lceil\frac2N\log_2\frac{3N!}{4}\right\rceil
\le t_{\rm mix}(d)\le Cd,
\qquad N=2^d.
\]
In particular $t_{\rm mix}(d)=\Theta(d)$, and its lower bound is
$2d-O(1)$.
There is an absolute P\ge2 such that for every dyadic n\ge2,
\operatorname{Tr}_{\rm reg}|Q_n|^P\le1+n^{-10}.
If v is an integer with 2v\ge P, then v independent sweeps have total-variation distance at most \frac12n^{-5} from uniform, from every deterministic initial deck. Here \|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|.
There is an absolute $P\ge2$ such that for every dyadic $n\ge2$,
\begin{equation}
\operatorname{Tr}_{\rm reg}|Q_n|^P\le1+n^{-10}.
\end{equation}
If $v$ is an integer with $2v\ge P$, then $v$ independent sweeps have total-variation distance at most $\frac12n^{-5}$ from uniform, from every deterministic initial deck. Here $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.
There are absolute constants L,C_0>0 such that the following holds. Put m=\sqrt n, assume m/2\le A,D\le2m, and take m sufficiently large that \theta=1-L/\log m>0. For all nonnegative functions w_i:S_D\to[0,\infty) and v_k:S_A\to[0,\infty),
\frac{n!}{|R||C|}\,
\mathbb E_U\!\left[\mathbf1_{\mathcal I}
\prod_{i=1}^A w_i(r_i)\prod_{k=1}^D v_k(c_k)\right]
\le e^{C_0n^{.54}}
\prod_{i=1}^A(\mathbb E w_i^{1/\theta})^\theta
\prod_{k=1}^D(\mathbb E v_k^{1/\theta})^\theta .
The expectations on the right are uniform on the indicated symmetric groups, and logarithms are natural.
There are absolute constants $L,C_0>0$ such that the following holds. Put $m=\sqrt n$, assume $m/2\le A,D\le2m$, and take $m$ sufficiently large that $\theta=1-L/\log m>0$. For all nonnegative functions $w_i:S_D\to[0,\infty)$ and $v_k:S_A\to[0,\infty)$,
\begin{equation}
\frac{n!}{|R||C|}\,
\mathbb E_U\!\left[\mathbf1_{\mathcal I}
\prod_{i=1}^A w_i(r_i)\prod_{k=1}^D v_k(c_k)\right]
\le e^{C_0n^{.54}}
\prod_{i=1}^A(\mathbb E w_i^{1/\theta})^\theta
\prod_{k=1}^D(\mathbb E v_k^{1/\theta})^\theta .
\end{equation}
The expectations on the right are uniform on the indicated symmetric groups, and logarithms are natural.
Theorem(A bounded regular moment)
There is an absolute finite p_*>0 such that, for every dyadic n,
Z_n(p_*)\le1+\frac1{16}.
For every integer M\ge p_*, M independent forward sweeps have worst-start total-variation distance at most 1/8 from uniform.
There is an absolute finite $p_*>0$ such that, for every dyadic $n$,
\begin{equation}
Z_n(p_*)\le1+\frac1{16}.
\end{equation}
For every integer $M\ge p_*$, $M$ independent forward sweeps have worst-start total-variation distance at most $1/8$ from uniform.
Corollary(Singular ranks and full-deck mixing)
For every nontrivial \lambda\vdash n and 1\le r\le D_\lambda,
s_r(T_{n,\lambda})\le(16D_\lambda r)^{-1/(2p_*)}.
If s_j(T_n) denotes the full regular singular list, including all multiplicities and zeros, then
s_j(T_n)\le j^{-1/(2p_*)}\qquad(1\le j\le n!).
The constant singular value is the first value. The physical Thorp chain has worst-start 1/4 mixing time \Theta(d); more precisely its lower bound is 2d-O(1). For every fixed integer M>p_*, the worst-start total-variation distance after Md physical shuffles tends to zero as d\to\infty.
For every nontrivial $\lambda\vdash n$ and $1\le r\le D_\lambda$,
\[
s_r(T_{n,\lambda})\le(16D_\lambda r)^{-1/(2p_*)}.
\]
If $s_j(T_n)$ denotes the full regular singular list, including all multiplicities and zeros, then
\[
s_j(T_n)\le j^{-1/(2p_*)}\qquad(1\le j\le n!).
\]
The constant singular value is the first value. The physical Thorp chain has worst-start $1/4$ mixing time $\Theta(d)$; more precisely its lower bound is $2d-O(1)$. For every fixed integer $M>p_*$, the worst-start total-variation distance after $Md$ physical shuffles tends to zero as $d\to\infty$.
Theorem(A moment bound for every signed occurrence)
For each sufficiently small fixed \bar\eta>0, choose a sufficiently small \bar\kappa>0 with \bar\kappa<\bar\eta/256. There is an integer r\ge1, depending only on these fixed constants, such that for every d\ge1, every \lambda\vdash n=2^d, and every occurrence (ten:spin:eq:1),
For each sufficiently small fixed $\bar\eta>0$, choose a sufficiently
small $\bar\kappa>0$ with $\bar\kappa<\bar\eta/256$. There is an
integer $r\ge1$, depending only on these fixed constants, such that for
every $d\ge1$, every $\lambda\vdash n=2^d$, and every
occurrence~\eqref{ten:spin:eq:1},
\begin{equation}
\log\!\left(D_\lambda\operatorname{Tr}_{V_\lambda}(B_n^*B_n)^r\right)
\le\eta_d F(\alpha,\beta)+g_n(l),
\end{equation}
where
\[
\eta_d=\bar\eta\left(1-\frac1{2\sqrt d}\right),\qquad
\kappa_d=\bar\kappa\left(1-\frac1{2\sqrt d}\right),\qquad
g_n(l)=\max\{0,\kappa_d l\log n-l\log(n/l)\}.
\]
Set $g_n(0)=0$ and interpret the logarithm of a zero trace as $-\infty$.
Corollary(Fixed-sweep convergence of the full deck)
There is an absolute positive integer $L$ such that
\[
\mathbb E_{U_{S_n}}|f_{d,L}-1|^2\longrightarrow0
\qquad(d\longrightarrow\infty).
\]
The convergence is uniform over starting orders. Moreover
$t_{\mathrm{mix}}(d)=\Theta(d)$.
There are absolute constants g>0 and d_0 such that, for d\ge d_0 and every \lambda\vdash 2^d,
\|K_\lambda\|_{\op}\le D_\lambda^{-g}.
The sign representation is annihilated. There is an absolute positive integer w such that the law after w independent sweeps converges to uniform in total variation as d\to\infty, uniformly over deterministic initial decks.
There are absolute constants \(g>0\) and \(d_0\) such that, for \(d\ge d_0\)
and every \(\lambda\vdash 2^d\),
\[
\|K_\lambda\|_{\op}\le D_\lambda^{-g}.
\]
The sign representation is annihilated. There is an absolute positive integer \(w\)
such that the law after \(w\) independent sweeps converges to uniform in
total variation as \(d\to\infty\), uniformly over deterministic initial
decks.
There are absolute constants $p_0\in(4/3,2)$ and $\varepsilon>0$ with the following property. Let $\nu$ be a probability measure on $S_4$ such that
\[
\|\nu-u\|_{\TV}<\varepsilon,
\qquad
\nu\{\pi:\pi(i)=j\}=\frac14\quad(1\le i,j\le4).
\]
Then every four nonnegative functions on $\{1,2,3,4\}$ satisfy
\begin{equation}
\E_\nu\prod_{i=1}^4f_i(\pi(i))\le\prod_{i=1}^4\|f_i\|_{p_0}.
\end{equation}
Theorem(A fixed moment with a degree saving)
There exist an even integer r\ge2 and \eta>0, independent of N, such that for every dyadic N and every \lambda\vdash N,
Consequently there is an absolute integer q for which the total-variation distance of q independent forward sweeps from uniform tends to zero as N\to\infty, uniformly over the starting deck.
There exist an even integer $r\ge2$ and $\eta>0$, independent of $N$, such that for every dyadic $N$ and every $\lambda\vdash N$,
\begin{equation}
D_\lambda\Tr B_N(\lambda)^r\le D_\lambda^{1-\eta}.
\end{equation}
Consequently there is an absolute integer $q$ for which the total-variation distance of $q$ independent forward sweeps from uniform tends to zero as $N\to\infty$, uniformly over the starting deck.
propext, Classical.choice, Quot.soundThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
18 local vocabulary declarations
Lines of Lean, without comments or blank lines
58
Second proof-verification program (nanoda)
Off in OpenAI's configuration.
Statement comparison
A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.
Plectis Atlas
Binary sweep contraction and mixing
Family 238: Optimal logarithmic mixing of the Thorp shuffle
Candidate pairing
Theorem (Binary sweep contraction)
There are absolute constants g>0 and d_0 such that, for d\ge d_0 and every \lambda\vdash 2^d,
\|K_\lambda\|_{\op}\le D_\lambda^{-g}.
The sign representation is annihilated. There is an absolute positive integer w such that the law after w independent sweeps converges to uniform in total variation as d\to\infty, uniformly over deterministic initial decks.
Conditional coordinate sweeps and analytic transfer
TeX label thm:binary, build/sections/01-introduction.tex, line 54
The Lean statement says
theorembinary_sweep_contraction_and_mixing : BinaryCoordinateSweeps.BinaryContractionTarget ∧ (∀ d : ℕ, 0 < d → ∑ g : Equiv.Perm (BinaryCoordinateSweeps.Slot d), BinaryCoordinateSweeps.binaryLaw d g * BinaryCoordinateSweeps.realSign g = 0) ∧ BinaryCoordinateSweeps.UniformSweepMixingTarget := bysorry
A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.
Recorded comparisons with the paper
Atlas records no contributed comparison of this statement with the paper.
Contributed Comparator run reports
Atlas records no contributed report of running Comparator for this statement file.