Lean statement

Polynomial-time query outside choiceless polynomial time

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.CPTSeparation.main

Lean statement file: ChoicelessPolynomialTime.leanShow on the mapFamily 243. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem main :    (∀ (A B : Type) [Fintype A] [Fintype B] (S : Input A) (T : Input B),      S.Iso T → (S.query ↔ T.query)) ∧    OrdinaryPolynomialTime ∧    ¬ FullCPT.EvaluationDefinable (fun {_} [_] I => I.query) := by  sorry

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.

abbreviation OAI.CPTSeparation.Scalar line 11
```
abbrev Scalar := ZMod 3
```

inductive type OAI.CPTSeparation.Symbol line 13

inductive Symbol  | Ed | Cf | EB | VB | I | Z (δ : Scalar)  deriving DecidableEq, Fintype

structure OAI.CPTSeparation.Input line 17

structure Input (A : Type) where  rel : Symbol → A → A → Bool

abbreviation OAI.CPTSeparation.Input.Edge line 24

abbrev Edge (S : Input A) := {y : A // S.rel .Ed y y = true}

abbreviation OAI.CPTSeparation.Input.Config line 26

abbrev Config (S : Input A) := {a : A // S.rel .Cf a a = true}

definition OAI.CPTSeparation.Input.coefficient line 32

def coefficient (S : Input A) (y : S.Edge) (a : S.Config) : Scalar :=  ∑ x : S.Edge, if S.rel .I a x then    ∑ δ : Scalar, if S.rel (.Z δ) y x then δ else 0    else 0

definition OAI.CPTSeparation.Input.incident line 37

def incident (S : Input A) (t : S.Config) (y : S.Edge) : Prop :=  ∃ a : S.Config, S.rel .VB t a = true ∧    ∃ x : S.Edge, S.rel .I a x = true ∧ S.rel .EB y x = true

definition OAI.CPTSeparation.Input.normalized line 41

def normalized (S : Input A) (lambda : S.Config → Scalar) : Prop :=  ∀ t : S.Config, (∑ a : S.Config, if S.rel .VB t a then lambda a else 0) = 1

definition OAI.CPTSeparation.Input.consistent line 44

def consistent (S : Input A) (lambda : S.Config → Scalar) (mu : S.Edge → Scalar) : Prop :=  ∀ (t : S.Config) (y : S.Edge), S.incident t y →    mu y = ∑ a : S.Config, if S.rel .VB t a then lambda a * S.coefficient y a else 0

definition OAI.CPTSeparation.Input.query line 48

def query (S : Input A) : Prop :=  ∃ (lambda : S.Config → Scalar) (mu : S.Edge → Scalar), S.normalized lambda ∧ S.consistent lambda mu

structure OAI.CPTSeparation.Input.Iso line 51

structure Iso (S : Input A) (T : Input B) extends A ≃ B where  rel_eq : ∀ r x y, T.rel r (toEquiv x) (toEquiv y) = S.rel r x y

abbreviation OAI.CPTSeparation.Hereditary.HF line 60

abbrev HF (A : Type uA) := Quotient (@Lists.instSetoidLists A)

definition OAI.CPTSeparation.Hereditary.mk line 66

def mk (l : Lists A) : HF A := Quotient.mk Lists.instSetoidLists l

definition OAI.CPTSeparation.Hereditary.atom line 68
```
def atom (a : A) : HF A := mk (Lists.atom a)
```

definition OAI.CPTSeparation.Hereditary.isSet line 70

def isSet (x : HF A) : Bool := Quotient.liftOn x (fun l => l.1)  (by intro l r h; cases h <;> rfl)

definition OAI.CPTSeparation.Hereditary.rawElements line 73

def rawElements (l : Lists A) : Finset (HF A) := by  classical  exact l.toList.toFinset.image mk

definition OAI.CPTSeparation.Hereditary.elements line 77

def elements (x : HF A) : Finset (HF A) := Quotient.liftOn x rawElements (by

Show the remaining 26 lines

  have mem_rawElements (a l : Lists A) : mk a ∈ rawElements l ↔ a ∈ l := by    classical    rcases l with ⟨(_ | _), l⟩    · cases l      change mk a ∈ (∅ : Finset (HF A)) ↔ False      simp    · change mk a ∈ (Lists'.toList l).toFinset.image mk ↔ a ∈ l      simp only [Finset.mem_image, List.mem_toFinset, Lists'.mem_def, mk, Quotient.eq]      constructor      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩  have raw_mem_congr_right {l r : Lists A} (h : Lists.Equiv l r) (a : Lists A) :      a ∈ l ↔ a ∈ r := by    cases h with    | refl => rfl    | antisymm hl hr =>      exact ⟨Lists'.mem_of_subset hl, Lists'.mem_of_subset hr⟩  intro l r h  ext z  induction z using Quotient.inductionOn with  | _ a =>    change mk a ∈ rawElements l ↔ mk a ∈ rawElements r    rw [mem_rawElements, mem_rawElements]    exact raw_mem_congr_right h a)

definition OAI.CPTSeparation.Hereditary.ofFinset line 107

def ofFinset (s : Finset (HF A)) : HF A :=  mk (Lists.ofList (s.toList.map Quotient.out))

definition OAI.CPTSeparation.Hereditary.rawRank' line 110

def rawRank' : {b : Bool} → Lists' A b → ℕ  | _, .atom _ => 0  | _, .nil => 0  | _, .cons' a l => max (rawRank' a + 1) (rawRank' l)

definition OAI.CPTSeparation.Hereditary.rawRank line 115
```
def rawRank (l : Lists A) : ℕ := rawRank' l.2
```

definition OAI.CPTSeparation.Hereditary.rank line 117

def rank (x : HF A) : ℕ := Quotient.liftOn x rawRank (by

Show the remaining 21 lines

  have rawRank_lt_of_mem {b : Bool} (l : Lists' A b) (a : Lists A)      (ha : a ∈ l.toList) : rawRank a < rawRank' l := by    induction l with    | atom => simp at ha    | nil => simp at ha    | cons' c l ihc ihl =>      rcases List.mem_cons.mp ha with rfl | ha      · exact lt_of_lt_of_le (Nat.lt_succ_self _) (le_max_left _ _)      · exact lt_of_lt_of_le (ihl ha) (le_max_right _ _)  have rawRank_congr {l r : Lists A} (h : Lists.Equiv l r) : rawRank l = rawRank r := by    induction h using Lists.Equiv.rec        (motive_2 := fun l r _ => rawRank' l ≤ rawRank' r) with    | refl => rfl    | antisymm hl hr ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r heq hmem hsub iheq ihsub =>      change max (rawRank a + 1) (rawRank' l) ≤ rawRank' r      refine max_le ?_ ihsub      rw [iheq]      exact rawRank_lt_of_mem r a' hmem  exact fun _ _ h => rawRank_congr h)

definition OAI.CPTSeparation.Hereditary.double line 146
```
def double (a b : HF A) : HF A := ofFinset {a,b}
```

definition OAI.CPTSeparation.Hereditary.ordinal line 148

def ordinal : ℕ → HF A  | 0 => ofFinset ∅  | i+1 => ofFinset (insert (ordinal i) (elements (ordinal i)))

abbreviation OAI.CPTSeparation.Operational.empty line 162
```
abbrev empty : HF A := ordinal 0
```

47 more definitions are reached the same way; the full file lists them.

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: decidable, definable, query, time, full, polynomial, relations and finite. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: eight, choiceless, isomorphism, structures, invariant and counting.

Theorem 1 of Choiceless polynomial time with counting does not capture polynomial time

Theorem

The query Q on all finite structures in the fixed vocabulary \tau of eight binary relations is isomorphism-invariant and decidable in deterministic polynomial time, but is not definable in full choiceless polynomial time with counting.

Section 1, Introduction Read it in the paper TeX source, line 81

Show the TeX

The query $Q$ on all finite structures in the fixed vocabulary $\tau$ of
eight binary relations is isomorphism-invariant and decidable in
deterministic polynomial time, but is not definable in full choiceless
polynomial time with counting.

Other possible paper matches, closest wording first

Theorem 1.1 of Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting. Words of the Lean statement, its names split into words, that also appear in the theorem: boolean, value, rank, polynomial, relations, cpt and one more. Found in the paper’s title, which its main theorem states: time. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: eight, hereditarily and counting.
Proposition 2 of Choiceless polynomial time with counting does not capture polynomial time. Words of the Lean statement, its names split into words, that also appear in the theorem: decidable, query, ordered, time, input and polynomial. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: isomorphism and invariant.
Proposition 4.4 of Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting. Words of the Lean statement, its names split into words, that also appear in the theorem: extends, consistent, guarded, state, input, polynomial and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: isomorphism and invariant.
Proposition 5.3 of Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting. Words of the Lean statement, its names split into words, that also appear in the theorem: chooses, pair, order, full, input, maps and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: outside, witnessing and choice.
Theorem 14 of Choiceless polynomial time with counting does not capture polynomial time. Words of the Lean statement, its names split into words, that also appear in the theorem: closure, hf, properties, max, relations, integers and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: object and structures.
Theorem 5.5 of Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting. Words of the Lean statement, its names split into words, that also appear in the theorem: evaluation, value and stated. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: gives.

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

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. 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.

Carlos Toledo’s cert-machine

How they ran it, in their words

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…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

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.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

Accepted Their term: “accepted”.
Re-run through Comparator with Lean’s kernel: accepted (the check took 302 s; peak memory 6.3 GiB).
Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

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.

Allowed axioms: propext, Quot.sound, Classical.choice

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 243’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.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: CPTSeparation.main : (∀ S T, S.Iso T → (S.query ↔ T.query)) ∧ OrdinaryPolynomialTime ∧ ¬ FullCPT.EvaluationDefinable (fun I => I.query), where query = consistency of an F₃ linear system coded by 8 relations, OrdinaryPolynomialTime uses Mathlib Turing.TM2ComputableInPolyTime with finite stack alphabets on ordered encodings, and EvaluationDefinable is polynomially bounded choiceless counting over hereditarily finite sets of arbitrary rank; and WitnessedChoice.main : ∃ φ, φ.formula.wscCount = 1 ∧ φ.BooleanOnAllInputs ∧ ∀ ψ, ψ.isCPT → φ.TrueModels ≠ ψ.TrueModels. Both separations of the summary are stated.
Definitions the group asks readers to compare with the paper: Custom 'choiceless polynomial time with counting', twice and in two different hand-written formalisms: FullCPT (ASM-style Program with Rule/Term over HF A = Lists A quotient, evaluationAccepts time space := ∃ h ≤ time(|A|), ... (P.occurring rel h).card ≤ space(|A|)) in ChoicelessPolynomialTime, and the term/formula logic WitnessedChoice.BGS (Term.iterate, resource p n := ⌊p(n)⌋₊, Formula.wsc, isCPT φ := wscCount = 0) in WitnessedChoice; the nonexpressibility statements are only as good as these encodings of CPTC. 'Polynomial time' for the query itself is Mathlib's standard TM2ComputableInPolyTime.
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalized result separates polynomial time from choiceless polynomial time with counting. It gives an explicit query on finite structures with eight relations that is invariant under isomorphism and decidable in polynomial time, but is not definable in the stated hereditarily finite-set language with cardinality and polynomial bounds on stages and intermediate objects. The query applies to all finite inputs without a promise. The separate witnessed-symmetric-choice result is not included.”
Quoted from OpenAI’s Lean note for this family

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

560 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: 332 to its own declarations, 225 to Mathlib’s documentation. 43 declared names also link to the same declaration in OpenAI’s library. 6 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInoncomputable sectionuniverse uA uB uC uF uRnamespace CPTSeparationabbrev Scalar := ZMod 3inductive Symbol  | Ed | Cf | EB | VB | I | Z (δ : Scalar)  deriving DecidableEq, Fintypestructure Input (A : Type) where  rel : Symbol → A → A → Boolnamespace Inputvariable {A B : Type} [Fintype A] [Fintype B]abbrev Edge (S : Input A) := {y : A // S.rel .Ed y y = true}abbrev Config (S : Input A) := {a : A // S.rel .Cf a a = true}instance (S : Input A) : Fintype S.Edge := inferInstanceAs (Fintype (Subtype _))instance (S : Input A) : Fintype S.Config := inferInstanceAs (Fintype (Subtype _))def coefficient (S : Input A) (y : S.Edge) (a : S.Config) : Scalar :=  ∑ x : S.Edge, if S.rel .I a x then    ∑ δ : Scalar, if S.rel (.Z δ) y x then δ else 0    else 0def incident (S : Input A) (t : S.Config) (y : S.Edge) : Prop :=  ∃ a : S.Config, S.rel .VB t a = true ∧    ∃ x : S.Edge, S.rel .I a x = true ∧ S.rel .EB y x = truedef normalized (S : Input A) (lambda : S.Config → Scalar) : Prop :=  ∀ t : S.Config, (∑ a : S.Config, if S.rel .VB t a then lambda a else 0) = 1def consistent (S : Input A) (lambda : S.Config → Scalar) (mu : S.Edge → Scalar) : Prop :=  ∀ (t : S.Config) (y : S.Edge), S.incident t y →    mu y = ∑ a : S.Config, if S.rel .VB t a then lambda a * S.coefficient y a else 0def query (S : Input A) : Prop :=  ∃ (lambda : S.Config → Scalar) (mu : S.Edge → Scalar), S.normalized lambda ∧ S.consistent lambda mustructure Iso (S : Input A) (T : Input B) extends A ≃ B where  rel_eq : ∀ r x y, T.rel r (toEquiv x) (toEquiv y) = S.rel r x yend Inputnamespace Hereditarysectionabbrev HF (A : Type uA) := Quotient (@Lists.instSetoidLists A)variable {A : Type uA} {B : Type uB}local instance instDecidableEqHF {A : Type uA} : DecidableEq (HF A) := Classical.decEq _def mk (l : Lists A) : HF A := Quotient.mk Lists.instSetoidLists ldef atom (a : A) : HF A := mk (Lists.atom a)def isSet (x : HF A) : Bool := Quotient.liftOn x (fun l => l.1)  (by intro l r h; cases h <;> rfl)def rawElements (l : Lists A) : Finset (HF A) := by  classical  exact l.toList.toFinset.image mkdef elements (x : HF A) : Finset (HF A) := Quotient.liftOn x rawElements (by  have mem_rawElements (a l : Lists A) : mk a ∈ rawElements l ↔ a ∈ l := by    classical    rcases l with ⟨(_ | _), l⟩    · cases l      change mk a ∈ (∅ : Finset (HF A)) ↔ False      simp    · change mk a ∈ (Lists'.toList l).toFinset.image mk ↔ a ∈ l      simp only [Finset.mem_image, List.mem_toFinset, Lists'.mem_def, mk, Quotient.eq]      constructor      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩  have raw_mem_congr_right {l r : Lists A} (h : Lists.Equiv l r) (a : Lists A) :      a ∈ l ↔ a ∈ r := by    cases h with    | refl => rfl    | antisymm hl hr =>      exact ⟨Lists'.mem_of_subset hl, Lists'.mem_of_subset hr⟩  intro l r h  ext z  induction z using Quotient.inductionOn with  | _ a =>    change mk a ∈ rawElements l ↔ mk a ∈ rawElements r    rw [mem_rawElements, mem_rawElements]    exact raw_mem_congr_right h a)instance : Membership (HF A) (HF A) := ⟨fun y x => x ∈ elements y⟩def ofFinset (s : Finset (HF A)) : HF A :=  mk (Lists.ofList (s.toList.map Quotient.out))def rawRank' : {b : Bool} → Lists' A b → ℕ  | _, .atom _ => 0  | _, .nil => 0  | _, .cons' a l => max (rawRank' a + 1) (rawRank' l)def rawRank (l : Lists A) : ℕ := rawRank' l.2def rank (x : HF A) : ℕ := Quotient.liftOn x rawRank (by  have rawRank_lt_of_mem {b : Bool} (l : Lists' A b) (a : Lists A)      (ha : a ∈ l.toList) : rawRank a < rawRank' l := by    induction l with    | atom => simp at ha    | nil => simp at ha    | cons' c l ihc ihl =>      rcases List.mem_cons.mp ha with rfl | ha      · exact lt_of_lt_of_le (Nat.lt_succ_self _) (le_max_left _ _)      · exact lt_of_lt_of_le (ihl ha) (le_max_right _ _)  have rawRank_congr {l r : Lists A} (h : Lists.Equiv l r) : rawRank l = rawRank r := by    induction h using Lists.Equiv.rec        (motive_2 := fun l r _ => rawRank' l ≤ rawRank' r) with    | refl => rfl    | antisymm hl hr ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r heq hmem hsub iheq ihsub =>      change max (rawRank a + 1) (rawRank' l) ≤ rawRank' r      refine max_le ?_ ihsub      rw [iheq]      exact rawRank_lt_of_mem r a' hmem  exact fun _ _ h => rawRank_congr h)endopen Classical Finsetvariable {A : Type uA} {B : Type uB}def double (a b : HF A) : HF A := ofFinset {a,b}def ordinal : ℕ → HF A  | 0 => ofFinset ∅  | i+1 => ofFinset (insert (ordinal i) (elements (ordinal i)))end Hereditarynamespace Operationalopen Classical Hereditary Finsetvariable {A : Type uA} {B : Type uB} {R : Type uR} {F : Type uF} {arity : F → ℕ}local instance instDecidableEqHF {C : Type uC} : DecidableEq (HF C) := Classical.decEq _abbrev empty : HF A := ordinal 0abbrev truth : HF A := ordinal 1def boolean (p : Prop) : HF A := if p then truth else emptydef inputRelation (rel : R → A → A → Bool) (r : R) (x y : HF A) : Prop :=  ∃ a b, x = atom a ∧ y = atom b ∧ rel r a b = truedef allAtoms [Fintype A] : HF A := ofFinset (univ.image atom)def unionHF (x : HF A) : HF A := ofFinset ((elements x).biUnion elements)def uniqueHF (x : HF A) : HF A :=  if h : ∃ a, elements x = {a} then h.choose else emptydef cardinalityHF (x : HF A) : HF A := ordinal (elements x).cardabbrev Location (F : Type uF) (arity : F → ℕ) (A : Type uA) := Σ f : F, Fin (arity f) → HF Astructure State (F : Type uF) (arity : F → ℕ) (A : Type uA) where  value : Location F arity A → HF A  finite : Set.Finite {l | value l ≠ empty}namespace Statedef initial : State F arity A := ⟨fun _ => empty, by simp⟩def support (s : State F arity A) : Finset (Location F arity A) := s.finite.toFinsetend Stateabbrev Update (F : Type uF) (arity : F → ℕ) (A : Type uA) := Location F arity A × HF Adef State.Consistent (u : Finset (Update F arity A)) : Prop :=  ∀ l x y, (l,x) ∈ u → (l,y) ∈ u → x = ydef State.updatedValue (s : State F arity A) (u : Finset (Update F arity A))    (l : Location F arity A) : HF A :=  if h : ∃ x, (l,x) ∈ u then h.choose else s.value ldef State.applyUpdates (s : State F arity A) (u : Finset (Update F arity A)) : State F arity A where  value := s.updatedValue u  finite := by    apply (s.finite.union (u.image Prod.fst).finite_toSet).subset    intro l hl    by_cases h : ∃ x, (l,x) ∈ u    · obtain ⟨x,hx⟩ := h      exact Or.inr (mem_image.mpr ⟨(l,x),hx,rfl⟩)    · exact Or.inl (by simpa only [Set.mem_ofPred_eq,updatedValue,dite_eq_right h] using hl)inductive Control | halt | accept deriving DecidableEqend Operationalsectionopen Classical Finsetvariable {A : Type uA} {B : Type uB}local instance Hereditary.instDecidableEqHF_1 {C : Type uC} : DecidableEq (HF C) := Classical.decEq _def Hereditary.closure (x : HF A) : Finset (HF A) :=  insert x ((elements x).attach.biUnion (fun y => closure y.val))termination_by rank xdecreasing_by  have mem_rawElements (a l : Lists A) : mk a ∈ rawElements l ↔ a ∈ l := by    classical    rcases l with ⟨(_ | _), l⟩    · cases l      change mk a ∈ (∅ : Finset (HF A)) ↔ False      simp    · change mk a ∈ (Lists'.toList l).toFinset.image mk ↔ a ∈ l      simp only [Finset.mem_image, List.mem_toFinset, Lists'.mem_def, mk, Quotient.eq]      constructor      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩      · rintro ⟨a',ha',heq⟩        exact ⟨a',ha',heq.symm⟩  have rawRank_lt_of_mem {b : Bool} (l : Lists' A b) (a : Lists A)      (ha : a ∈ l.toList) : rawRank a < rawRank' l := by    induction l with    | atom => simp at ha    | nil => simp at ha    | cons' c l ihc ihl =>      rcases List.mem_cons.mp ha with rfl | ha      · exact lt_of_lt_of_le (Nat.lt_succ_self _) (le_max_left _ _)      · exact lt_of_lt_of_le (ihl ha) (le_max_right _ _)  have rawRank_congr {l r : Lists A} (h : Lists.Equiv l r) : rawRank l = rawRank r := by    induction h using Lists.Equiv.rec        (motive_2 := fun l r _ => rawRank' l ≤ rawRank' r) with    | refl => rfl    | antisymm _hl _hr ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r _heq hmem _hsub iheq ihsub =>      change max (rawRank a + 1) (rawRank' l) ≤ rawRank' r      refine max_le ?_ ihsub      rw [iheq]      exact rawRank_lt_of_mem r a' hmem  have rank_lt_of_mem {x y : HF A} (h : x ∈ y) : rank x < rank y := by    induction y using Quotient.inductionOn with    | _ l =>      induction x using Quotient.inductionOn with      | _ a =>        have h' := (mem_rawElements a l).mp h        rcases l with ⟨(_ | _), l⟩        · exact False.elim h'        · obtain ⟨a',ha',heq⟩ := h'          change rawRank a < rawRank' l          rw [rawRank_congr heq]          exact rawRank_lt_of_mem l a' ha'  exact rank_lt_of_mem y.propertydef Hereditary.familyClosure (f : Finset (HF A)) : Finset (HF A) := f.biUnion closureendsectionopen Classical Hereditary Finsetvariable {A : Type uA} {R : Type uR} {F : Type uF} {arity : F → ℕ}local instance Operational.instDecidableEqHF_1 {C : Type uC} : DecidableEq (HF C) := Classical.decEq _def Operational.State.critical (s : State F arity A) : Finset (HF A) :=  s.support.biUnion (fun l => insert (s.value l) (univ.image l.2))def Operational.State.active [Fintype A] (s : State F arity A) : Finset (HF A) :=  familyClosure (s.critical ∪ {allAtoms,empty,truth} ∪ univ.image atom)endnamespace FullCPTsectionopen Classical Hereditary Finsetopen Operational (State Control Location Update)local instance instDecidableEqHF {C : Type} : DecidableEq (HF C) := Classical.decEq _inductive Term (R F : Type) (arity : F → ℕ) : Type  | var (name : ℕ)  | ordinal (n : ℕ)  | atoms  | app (f : F) (args : Fin (arity f) → Term R F arity)  | pair (a b : Term R F arity)  | union (a : Term R F arity)  | unique (a : Term R F arity)  | card (a : Term R F arity)  | equal (a b : Term R F arity)  | member (a b : Term R F arity)  | isAtom (a : Term R F arity)  | input (r : R) (a b : Term R F arity)  | not (a : Term R F arity)  | and (a b : Term R F arity)  | or (a b : Term R F arity)  | conditional (c a b : Term R F arity)  | comprehend (name : ℕ) (bound guard body : Term R F arity)variable {A R F : Type} {arity : F → ℕ}namespace Termvariable [Fintype A]def eval (rel : R → A → A → Bool) (s : State F arity A) :    Term R F arity → (ℕ → HF A) → HF A  | .var n, v => v n  | .ordinal n, _ => Hereditary.ordinal n  | .atoms, _ => Operational.allAtoms  | .app f args, v => s.value ⟨f, fun i => eval rel s (args i) v⟩  | .pair a b, v => double (eval rel s a v) (eval rel s b v)  | .union a, v => Operational.unionHF (eval rel s a v)  | .unique a, v => Operational.uniqueHF (eval rel s a v)  | .card a, v => Operational.cardinalityHF (eval rel s a v)  | .equal a b, v => Operational.boolean (eval rel s a v = eval rel s b v)  | .member a b, v => Operational.boolean (eval rel s a v ∈ eval rel s b v)  | .isAtom a, v => Operational.boolean (isSet (eval rel s a v) = false)  | .input r a b, v => Operational.boolean (Operational.inputRelation rel r (eval rel s a v) (eval rel s b v))  | .not a, v => Operational.boolean (eval rel s a v ≠ Operational.truth)  | .and a b, v => Operational.boolean (eval rel s a v = Operational.truth ∧ eval rel s b v = Operational.truth)  | .or a b, v => Operational.boolean (eval rel s a v = Operational.truth ∨ eval rel s b v = Operational.truth)  | .conditional c a b, v => if eval rel s c v = Operational.truth then eval rel s a v else eval rel s b v  | .comprehend n bound guard body, v =>      ofFinset (((elements (eval rel s bound v)).filter        (fun x => eval rel s guard (Function.update v n x) = Operational.truth)).image        (fun x => eval rel s body (Function.update v n x)))end Terminductive Rule (R F : Type) (arity : F → ℕ) : Type  | skip  | update (f : F) (args : Fin (arity f) → Term R F arity) (value : Term R F arity)  | parallel (a b : Rule R F arity)  | conditional (condition : Term R F arity) (a b : Rule R F arity)  | forall (name : ℕ) (bound : Term R F arity) (body : Rule R F arity)  | letValue (name : ℕ) (value : Term R F arity) (body : Rule R F arity)namespace Ruledef updates [Fintype A] (rel : R → A → A → Bool) (s : State F arity A) :    Rule R F arity → (ℕ → HF A) → Finset (Update F arity A)  | .skip, _ => ∅  | .update f args value, v => {(⟨f, fun i => (args i).eval rel s v⟩, value.eval rel s v)}  | .parallel a b, v => updates rel s a v ∪ updates rel s b v  | .conditional c a b, v => if c.eval rel s v = Operational.truth then updates rel s a v else updates rel s b v  | .forall n bound body, v => (elements (bound.eval rel s v)).biUnion      (fun x => updates rel s body (Function.update v n x))  | .letValue n value body, v => updates rel s body (Function.update v n (value.eval rel s v))end Rulestructure Program (R : Type) where  Functions : Type  finiteFunctions : Fintype Functions  arity : Functions → ℕ  body : Rule R (Control ⊕ Functions) (Sum.elim (fun _ => 0) arity)namespace Programvariable (P : Program R) [Fintype A]abbrev functionArity : Control ⊕ P.Functions → ℕ := Sum.elim (fun _ => 0) P.arityabbrev Store := State (Control ⊕ P.Functions) P.functionArity Adef flag (s : P.Store (A := A)) (c : Control) : Prop := s.value ⟨.inl c, Fin.elim0⟩ = Operational.truthdef step (rel : R → A → A → Bool) (s : P.Store (A := A)) : Option (P.Store (A := A)) :=  if P.flag s .halt then some s else    let u := P.body.updates rel s (fun _ => Operational.empty)    if State.Consistent u then some (s.applyUpdates u) else nonedef run (rel : R → A → A → Bool) : ℕ → Option (P.Store (A := A))  | 0 => some State.initial  | j+1 => (run rel j).bind (P.step rel)def active (rel : R → A → A → Bool) (h : ℕ) : Finset (HF A) :=  (Finset.range (h+1)).biUnion (fun j => ((P.run rel j).toFinset).biUnion State.active)end Programendopen Classical Hereditary Finsetopen Operational (State Control)local instance instDecidableEqHF_1 {C : Type} : DecidableEq (HF C) := Classical.decEq _variable {A R F : Type} {arity : F → ℕ}sectionvariable [Fintype A]def Term.roots (rel : R → A → A → Bool) (s : State F arity A) :    Term R F arity → (ℕ → HF A) → Finset (HF A)  | t@(.var _), v | t@(.ordinal _), v | t@(.atoms), v => {t.eval rel s v}  | t@(.app _ args), v => insert (t.eval rel s v)      ((List.ofFn (fun i => roots rel s (args i) v)).foldr (· ∪ ·) ∅)  | t@(.pair a b), v | t@(.equal a b), v | t@(.member a b), v  | t@(.input _ a b), v | t@(.and a b), v | t@(.or a b), v =>      insert (t.eval rel s v) (roots rel s a v ∪ roots rel s b v)  | t@(.union a), v | t@(.unique a), v | t@(.card a), v  | t@(.isAtom a), v | t@(.not a), v => insert (t.eval rel s v) (roots rel s a v)  | .conditional c a b, v => roots rel s c v ∪      if c.eval rel s v = Operational.truth then roots rel s a v else roots rel s b v  | t@(.comprehend n bound guard body), v => insert (t.eval rel s v)      (roots rel s bound v ∪ (elements (bound.eval rel s v)).biUnion (fun x =>        roots rel s guard (Function.update v n x) ∪        if guard.eval rel s (Function.update v n x) = Operational.truth then          roots rel s body (Function.update v n x) else ∅))def Rule.roots (rel : R → A → A → Bool) (s : State F arity A) : Rule R F arity → (ℕ → HF A) → Finset (HF A) | .skip, _ => ∅ | .update _ args value, v => value.roots rel s v ∪     (List.ofFn (fun i => (args i).roots rel s v)).foldr (· ∪ ·) ∅ | .parallel a b, v => roots rel s a v ∪ roots rel s b v | .conditional c a b, v => c.roots rel s v ∪     if c.eval rel s v = Operational.truth then roots rel s a v else roots rel s b v | .forall n bound body, v => bound.roots rel s v ∪     (elements (bound.eval rel s v)).biUnion (fun x => roots rel s body (Function.update v n x)) | .letValue n value body, v => value.roots rel s v ∪     roots rel s body (Function.update v n (value.eval rel s v))endsectionvariable (P : Program R) [Fintype A]def Program.stepRoots (rel : R → A → A → Bool) (s : P.Store (A := A)) : Finset (HF A) := if P.flag s .halt then ∅ else P.body.roots rel s (fun _ => Operational.empty)def Program.occurring (rel : R → A → A → Bool) (h : ℕ) : Finset (HF A) := P.active rel h ∪ (range h).biUnion (fun j => match P.run rel j with   | none => ∅   | some s => familyClosure (P.stepRoots rel s))def Program.evaluationAccepts (time space : Polynomial ℕ) (rel : R → A → A → Bool) : Prop := ∃ h st, h ≤ time.eval (Fintype.card A) ∧ P.run rel h = some st ∧ P.flag st .halt ∧ P.flag st .accept ∧   (P.occurring rel h).card ≤ space.eval (Fintype.card A)enddef EvaluationDefinable (Q : ∀ {A : Type}, [Fintype A] → Input A → Prop) : Prop := ∃ P : Program Symbol, ∃ time space : Polynomial ℕ,   ∀ (A : Type) [Fintype A] (I : Input A), P.evaluationAccepts time space I.rel ↔ Q Iend FullCPTnamespace OrderedQuerysectionopen Finsetvariable {N : ℕ}abbrev Data (N : ℕ) := Input (Fin N)enddef indexSymbol (i : Fin 8) : Symbol :=  if i.val = 0 then .Ed else  if i.val = 1 then .Cf else  if i.val = 2 then .EB else  if i.val = 3 then .VB else  if i.val = 4 then .I else .Z ((i.val-5 : ℕ) : Scalar)variable {N : ℕ}def cellValue (S : Data N) (k : Fin (8*(N*N))) : Bool :=  let ij := finProdFinEquiv.symm k  let ab := finProdFinEquiv.symm ij.2  S.rel (indexSymbol ij.1) ab.1 ab.2def tableBits (S : Data N) : List Bool := List.ofFn (cellValue S)abbrev OrderedInput := Σ N, Data Nend OrderedQuerynamespace GaussMachineabbrev Letter := Option Scalardef boolCode (b : Bool) : List Letter := [some (if b then 1 else 0)]end GaussMachinenamespace CounterLangabbrev Letter := Option Scalarend CounterLangnamespace TableMachineopen CounterLangdef bitLetter (b : Bool) : Letter := some (if b then 1 else 0)def tableInput {N} (S : OrderedQuery.Data N) : List Letter := (OrderedQuery.tableBits S).map bitLetterdef code (S : OrderedQuery.OrderedInput) : List Letter := List.replicate S.1 none ++ some 0 :: tableInput S.2end TableMachinedef Input.ordered {A : Type} {N : ℕ} (S : Input A) (e : A ≃ Fin N) : OrderedQuery.Data N :=  ⟨fun r i j => S.rel r (e.symm i) (e.symm j)⟩def OrdinaryPolynomialTime : Prop :=  ∃ answer : OrderedQuery.OrderedInput → Bool,    ∃ machine : Turing.TM2ComputableInPolyTime TableMachine.code GaussMachine.boolCode answer,      (∀ k, Finite (machine.tm.Γ k)) ∧      ∀ (A : Type) [Fintype A] (N : ℕ) (e : A ≃ Fin N) (S : Input A),        answer ⟨N,S.ordered e⟩ = true ↔ S.querytheorem main :    (∀ (A B : Type) [Fintype A] [Fintype B] (S : Input A) (T : Input B),      S.Iso T → (S.query ↔ T.query)) ∧    OrdinaryPolynomialTime ∧    ¬ FullCPT.EvaluationDefinable (fun {_} [_] I => I.query) := by  sorryend CPTSeparationendend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Choiceless polynomial time with counting does not capture polynomial time

Theorem

Section 1, Introduction Read it in the paper TeX source, line 81

Show the TeX

The query $Q$ on all finite structures in the fixed vocabulary $\tau$ of
eight binary relations is isomorphism-invariant and decidable in
deterministic polynomial time, but is not definable in full choiceless
polynomial time with counting.

Proposition

The query Q is isomorphism-invariant and decidable in deterministic polynomial time from an ordered encoding of its input structure.

Section 1, Introduction Read it in the paper TeX source, line 93

Show the TeX

The query $Q$ is isomorphism-invariant and decidable in deterministic
polynomial time from an ordered encoding of its input structure.

Corollary

On nonempty finite \tau-structures, Q is definable in both \mathrm{FPS}_3 and \mathrm{FPR}_3. Consequently neither of these logics is contained in \CPT.

Section 1, Introduction Read it in the paper TeX source, line 123

Show the TeX

On nonempty finite $\tau$-structures, $Q$ is definable in both
$\mathrm{FPS}_3$ and $\mathrm{FPR}_3$. Consequently neither of these
logics is contained in $\CPT$.

Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting

Theorem

There exist a vocabulary \tau of eight binary relations, a fixed polynomial p, and a \CPT+\WSC sentence (\Phi,p) with one occurrence of a WSC operator such that:

(i)
(\Phi,p) has a Boolean value on every finite \tau-structure;
(ii)
no \CPT sentence over \tau has the same true-model class.

The \CPT sentences in (ii) may use counting and hereditarily finite sets of unrestricted finite rank.

Section 1, Introduction Read it in the paper TeX source, line 38

Show the TeX

There exist a vocabulary \(\tau\) of eight binary relations, a fixed polynomial
\(p\), and a \(\CPT+\WSC\) sentence \((\Phi,p)\) with one occurrence of a WSC
operator such that:
\begin{enumerate}[label=\textup{(\roman*)}]
\item \((\Phi,p)\) has a Boolean value on every finite \(\tau\)-structure;
\item no \(\CPT\) sentence over \(\tau\) has the same true-model class.
\end{enumerate}
The \(\CPT\) sentences in \textup{(ii)} may use counting and hereditarily
finite sets of unrestricted finite rank.

Configuration and file facts

File: lean/ComparatorChallenges/ChoicelessPolynomialTime.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/ModelTheory/Choiceless/Separation.lean
Allowed axioms: propext, Quot.sound, Classical.choiceThe 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: 83 local vocabulary declarations
Lines of Lean, without comments or blank lines: 337
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas