Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Strict expressive gain from one witnessed symmetric choice

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

Lean statement file: WitnessedChoice.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 243 link it.

See the candidate theoremWho ran the proof-verification programReport 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.

def MainStatement : Prop := ∃ φ : Sentence,  φ.formula.wscCount = 1 ∧ φ.BooleanOnAllInputs ∧    ∀ ψ : Sentence, ψ.isCPT → φ.TrueModels ≠ ψ.TrueModelstheorem WitnessedChoice.main : WitnessedChoice.BGS.MainStatement := 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.WitnessedSeparation.Hereditary.HF line 13

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

  • definition OAI.WitnessedSeparation.Hereditary.mk line 21

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

  • definition OAI.WitnessedSeparation.Hereditary.atom line 23

    def atom (a : A) : HF A := mk (Lists.atom a)

  • definition OAI.WitnessedSeparation.Hereditary.rawElements line 28

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

  • definition OAI.WitnessedSeparation.Hereditary.elements line 32

    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.WitnessedSeparation.Hereditary.ofFinset line 62

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

  • definition OAI.WitnessedSeparation.Hereditary.rawRank' line 65

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

  • definition OAI.WitnessedSeparation.Hereditary.rawRank line 70

    def rawRank (l : Lists A) : ℕ := rawRank' l.2

  • definition OAI.WitnessedSeparation.Hereditary.rank line 72

    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 _ _ ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r _ hmem _ 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.WitnessedSeparation.Hereditary.rawMap' line 95

    def rawMap' (f : A → B) : {b : Bool} → Lists' A b → Lists' B b  | _, .atom a => .atom (f a)  | _, .nil => .nil  | _, .cons' a l => .cons' (rawMap' f a) (rawMap' f l)

  • definition OAI.WitnessedSeparation.Hereditary.rawMap line 100

    def rawMap (f : A → B) (l : Lists A) : Lists B := ⟨l.1, rawMap' f l.2⟩

  • definition OAI.WitnessedSeparation.Hereditary.map line 102

    def map (f : A → B) (x : HF A) : HF B := by
    Show the remaining 18 lines
      have toList_rawMap' (f : A → B) {b : Bool} (l : Lists' A b) :      (rawMap' f l).toList = l.toList.map (rawMap f) := by    induction l with    | atom => rfl    | nil => rfl    | cons' a l iha ihl => simp only [rawMap', Lists'.toList, ihl]; rfl  have rawMap_congr (f : A → B) {l r : Lists A} (h : Lists.Equiv l r) :      Lists.Equiv (rawMap f l) (rawMap f r) := by    induction h using Lists.Equiv.rec        (motive_2 := fun l r _ => Lists'.Subset (rawMap' f l) (rawMap' f r)) with    | refl => exact Lists.Equiv.refl _    | antisymm hl hr ihl ihr => exact Lists.Equiv.antisymm ihl ihr    | nil => exact Lists'.Subset.nil    | @cons a a' l r _ hmem _ iheq ihsub =>      apply Lists'.Subset.cons iheq _ ihsub      rw [toList_rawMap']      exact List.mem_map.mpr ⟨a',hmem,rfl⟩  exact Quotient.liftOn x (fun l => mk (rawMap f l)) (fun _ _ h => Quotient.eq.mpr (rawMap_congr f h))

  • definition OAI.WitnessedSeparation.Hereditary.singleton line 169

    def singleton (a : HF A) : HF A := ofFinset {a}

  • definition OAI.WitnessedSeparation.Hereditary.double line 171

    def double (a b : HF A) : HF A := ofFinset {a,b}

  • definition OAI.WitnessedSeparation.Hereditary.pair line 173

    def pair (a b : HF A) : HF A := double (singleton a) (double a b)

  • definition OAI.WitnessedSeparation.Hereditary.ordinal line 175

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

  • definition OAI.WitnessedSeparation.Hereditary.closure line 181

    def closure (x : HF A) : Finset (HF A) :=
    Show the remaining 49 lines
      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 _ _ ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r _ hmem _ 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.property

  • abbreviation OAI.WitnessedSeparation.Scalar line 234

    abbrev Scalar := ZMod 3

  • inductive type OAI.WitnessedSeparation.Symbol line 236

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

  • structure OAI.WitnessedSeparation.Input line 240

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

  • inductive type OAI.WitnessedChoice.BGS.Term line 253

    inductive Term : ℕ → Type    | var {n} (i : Fin n) : Term n    | empty {n} : Term n    | atoms {n} : Term n
    Show the remaining 7 lines
        | pair {n} (a b : Term n) : Term n    | union {n} (a : Term n) : Term n    | unique {n} (a : Term n) : Term n    | card {n} (a : Term n) : Term n    | comprehend {n} (body : Term (n+1)) (range : Term n)        (guard : Formula (n+1)) : Term n    | iterate {n} (step : Term (n+1)) : Term n

  • inductive type OAI.WitnessedChoice.BGS.Formula line 264

      inductive Formula : ℕ → Type    | equal {n} (a b : Term n) : Formula n    | input {n} (r : Symbol) (a b : Term n) : Formula n    | neg {n} (a : Formula n) : Formula n    | and {n} (a b : Formula n) : Formula n    | or {n} (a b : Formula n) : Formula n    | wsc {n} (step : Term (n+2)) (choice : Term (n+1))        (witness : Term (n+2)) (output : Formula (n+1)) : Formula n

  • definition OAI.WitnessedChoice.BGS.Term.wscCount line 298

    def Term.wscCount : {n : ℕ} → Term n → ℕ    | _, .var _ | _, .empty | _, .atoms => 0    | _, .pair a b => a.wscCount + b.wscCount    | _, .union a | _, .unique a | _, .card a => a.wscCount    | _, .comprehend body range guard => body.wscCount + range.wscCount + guard.wscCount    | _, .iterate step => step.wscCount

  • abbreviation OAI.WitnessedChoice.BGS.Result line 315

    abbrev Result (α : Type) := Option α

16 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: boolean, wsc, model, polynomial, relations, cpt, counting, sentences and one more. Found in the paper’s title, which its main theorem states: witnessed and choice. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: occurrence and one.

Statements in Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting come first because the release’s name for this Lean statement shares words with that paper’s title.

Theorem 1.1 of 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:

  1. (i)

    (\Phi,p) has a Boolean value on every finite \tau-structure;

  2. (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.

Other possible paper matches, closest wording first

  • 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: pair, witnessing, choice, input, maps and atom. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: one.
  • 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: guarded, wsc, model, input, polynomial, cpt and two more.
  • Theorem 9.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: models, cpt, counting and sentence.
  • Proposition 3.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: scalar and maps.
  • Theorem 1 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, polynomial, relations, counting and finite. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: choiceless, definable and time.
  • Corollary 6.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: atoms and finite. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: exactly.

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 184 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 formalization proves that witnessed symmetric choice strictly increases the expressive power of choiceless polynomial time with counting. It constructs one fixed sentence with exactly one witnessed-choice occurrence that gives a Boolean answer on every finite input, while no sentence of the original counting formalism defines the same class of inputs.”

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

474 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: 353 to its own declarations, 221 to Mathlib’s documentation. 14 declared names also link to the same declaration in OpenAI’s library. 3 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. 3 of them could name more than one declaration. 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 u v wnamespace WitnessedSeparationnamespace Hereditaryabbrev HF (A : Type u) := Quotient (@Lists.instSetoidLists A)variable {A : Type u} {B : Type v}sectionlocal instance {A : Type u} : 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 _ _ ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r _ hmem _ 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)def rawMap' (f : A → B) : {b : Bool} → Lists' A b → Lists' B b  | _, .atom a => .atom (f a)  | _, .nil => .nil  | _, .cons' a l => .cons' (rawMap' f a) (rawMap' f l)def rawMap (f : A → B) (l : Lists A) : Lists B := ⟨l.1, rawMap' f l.2⟩def map (f : A → B) (x : HF A) : HF B := by  have toList_rawMap' (f : A → B) {b : Bool} (l : Lists' A b) :      (rawMap' f l).toList = l.toList.map (rawMap f) := by    induction l with    | atom => rfl    | nil => rfl    | cons' a l iha ihl => simp only [rawMap', Lists'.toList, ihl]; rfl  have rawMap_congr (f : A → B) {l r : Lists A} (h : Lists.Equiv l r) :      Lists.Equiv (rawMap f l) (rawMap f r) := by    induction h using Lists.Equiv.rec        (motive_2 := fun l r _ => Lists'.Subset (rawMap' f l) (rawMap' f r)) with    | refl => exact Lists.Equiv.refl _    | antisymm hl hr ihl ihr => exact Lists.Equiv.antisymm ihl ihr    | nil => exact Lists'.Subset.nil    | @cons a a' l r _ hmem _ iheq ihsub =>      apply Lists'.Subset.cons iheq _ ihsub      rw [toList_rawMap']      exact List.mem_map.mpr ⟨a',hmem,rfl⟩  exact Quotient.liftOn x (fun l => mk (rawMap f l)) (fun _ _ h => Quotient.eq.mpr (rawMap_congr f h))instance {G : Type w} [Group G] [MulAction G A] : MulAction G (HF A)  := by  have map_mk {A B : Type u} (f : A → B) (l : Lists A) : map f (mk l) = mk (rawMap f l) := rfl  have rawMap_id {A : Type u} : ∀ l : Lists A, rawMap id l = l := by    rintro ⟨b,l⟩    have h : rawMap' id l = l := by      induction l with      | atom => rfl      | nil => rfl      | cons' a l iha ihl => simp only [rawMap', iha,ihl]    exact congrArg (Sigma.mk b) h  have map_id {A : Type u} (x : HF A) : map id x = x := by    induction x using Quotient.inductionOn with    | _ l =>      change map id (mk l) = mk l      rw [map_mk, rawMap_id]  have rawMap_comp {A B : Type u} {C : Type u} (g : B → C) (f : A → B) (l : Lists A) :      rawMap g (rawMap f l) = rawMap (g ∘ f) l := by    rcases l with ⟨b,l⟩    have h : rawMap' g (rawMap' f l) = rawMap' (g ∘ f) l := by      induction l with      | atom => rfl      | nil => rfl      | cons' a l iha ihl => simp only [rawMap', iha,ihl]    exact congrArg (Sigma.mk b) h  have map_comp {A B : Type u} {C : Type u} (g : B → C) (f : A → B) (x : HF A) :      map g (map f x) = map (g ∘ f) x := by    induction x using Quotient.inductionOn with    | _ l =>      change map g (map f (mk l)) = map (g ∘ f) (mk l)      simp only [map_mk,rawMap_comp]  exact {    smul g x := map (fun a => g • a) x    one_smul x := by      change map (fun a : A => (1 : G) • a) x = x      have h : (fun a : A => (1 : G) • a) = id := by funext a; simp      rw [h,map_id]    mul_smul g h x := by      change map (fun a : A => (g*h) • a) x = map (fun a => g • a) (map (fun a => h • a) x)      rw [map_comp]      congr 1      funext a      exact mul_smul g h a }endopen Classical Finsetdef singleton (a : HF A) : HF A := ofFinset {a}def double (a b : HF A) : HF A := ofFinset {a,b}def pair (a b : HF A) : HF A := double (singleton a) (double a b)def ordinal : ℕ → HF A  | 0 => ofFinset ∅  | i+1 => ofFinset (insert (ordinal i) (elements (ordinal i)))local instance {C : Type w} : DecidableEq (HF C) := Classical.decEq _def 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 _ _ ihl ihr => exact Nat.le_antisymm ihl ihr    | nil => exact Nat.zero_le _    | @cons a a' l r _ hmem _ 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.propertyend Hereditaryabbrev Scalar := ZMod 3inductive Symbol  | Ed | Cf | EB | VB | I | Z (δ : Scalar)  deriving DecidableEq, Fintypestructure Input (A : Type) where  rel : Symbol → A → A → Boolend WitnessedSeparationnamespace WitnessedChoicenamespace BGSopen Classical WitnessedSeparation WitnessedSeparation.Hereditarymutualinductive Term : ℕ → Type    | var {n} (i : Fin n) : Term n    | empty {n} : Term n    | atoms {n} : Term n    | pair {n} (a b : Term n) : Term n    | union {n} (a : Term n) : Term n    | unique {n} (a : Term n) : Term n    | card {n} (a : Term n) : Term n    | comprehend {n} (body : Term (n+1)) (range : Term n)        (guard : Formula (n+1)) : Term n    | iterate {n} (step : Term (n+1)) : Term n  inductive Formula : ℕ → Type    | equal {n} (a b : Term n) : Formula n    | input {n} (r : Symbol) (a b : Term n) : Formula n    | neg {n} (a : Formula n) : Formula n    | and {n} (a b : Formula n) : Formula n    | or {n} (a b : Formula n) : Formula n    | wsc {n} (step : Term (n+2)) (choice : Term (n+1))        (witness : Term (n+2)) (output : Formula (n+1)) : Formula nenddef dropFree {n} (f : Finset (Fin (n+1))) : Finset (Fin n) :=  Finset.univ.filter (fun i => i.succ ∈ f)mutualdef Term.free : {n : ℕ} → Term n → Finset (Fin n)    | _, .var i => {i}    | _, .empty | _, .atoms => ∅    | _, .pair a b => a.free ∪ b.free    | _, .union a | _, .unique a | _, .card a => a.free    | _, .comprehend body range guard => range.free ∪ dropFree (body.free ∪ guard.free)    | _, .iterate step => dropFree step.free  def Formula.free : {n : ℕ} → Formula n → Finset (Fin n)    | _, .equal a b | _, .input _ a b => a.free ∪ b.free    | _, .neg a => a.free    | _, .and a b | _, .or a b => a.free ∪ b.free    | _, .wsc step choice witness output =>        dropFree (dropFree (step.free ∪ witness.free)) ∪ dropFree (choice.free ∪ output.free)endmutualdef Term.wscCount : {n : ℕ} → Term n → ℕ    | _, .var _ | _, .empty | _, .atoms => 0    | _, .pair a b => a.wscCount + b.wscCount    | _, .union a | _, .unique a | _, .card a => a.wscCount    | _, .comprehend body range guard => body.wscCount + range.wscCount + guard.wscCount    | _, .iterate step => step.wscCount  def Formula.wscCount : {n : ℕ} → Formula n → ℕ    | _, .equal a b | _, .input _ a b => a.wscCount + b.wscCount    | _, .neg a => a.wscCount    | _, .and a b | _, .or a b => a.wscCount + b.wscCount    | _, .wsc step choice witness output =>        1 + step.wscCount + choice.wscCount + witness.wscCount + output.wscCountendvariable {A : Type}abbrev Result (α : Type) := Option αdef emptyHF : HF A := ofFinset ∅def TC (x : HF A) : Finset (HF A) := (elements x).biUnion closuredef unionHF (x : HF A) : HF A := ofFinset ((elements x).biUnion elements)def uniqueHF (x : HF A) : HF A :=  if h : ∃ y, elements x = {y} then h.choose else emptyHFdef cardHF (x : HF A) : HF A := ordinal (elements x).carddef inputHF (S : Input A) (r : Symbol) (x y : HF A) : Bool :=  decide (∃ a b, x = atom a ∧ y = atom b ∧ S.rel r a b = true)def lift₂ {X Y Z : Type} (f : X → Y → Z) (a : Result X) (b : Result Y) : Result Z :=  a.bind (fun x => b.map (f x))def collect (r : HF A) (guard : HF A → Result Bool) (body : HF A → Result (HF A)) :    Result (HF A) :=  if (∀ x ∈ elements r, (guard x).isSome) ∧      (∀ x ∈ elements r, guard x = some true → (body x).isSome) then    some (ofFinset (((elements r).filter (fun x => guard x = some true)).image      (fun x => (body x).getD emptyHF)))  else nonedef iterationLoop (p : ℕ) (step : HF A → Result (HF A)) : ℕ → HF A → Result (HF A)  | 0, _ => some emptyHF  | fuel+1, x =>      if (TC x).card ≤ p then        (step x).bind (fun y =>          if x = y then some x else iterationLoop p step fuel y)      else some emptyHFdef ordinaryIteration (p : ℕ) (step : HF A → Result (HF A)) : Result (HF A) :=  iterationLoop p step (p+1) emptyHFdef resource (p : Polynomial ℝ) (n : ℕ) : ℕ := ⌊p.eval (n : ℝ)⌋₊variable [Fintype A]def permutationGraph (g : Equiv.Perm A) : HF A :=  ofFinset (Finset.univ.image (fun a => pair (atom a) (atom (g a))))def Automorphism (S : Input A) (g : Equiv.Perm A) : Prop :=  ∀ r a b, S.rel r (g a) (g b) = S.rel r a bdef ChoicePrefix (step : HF A → HF A → Result (HF A))    (choice : HF A → Result (HF A)) (b c : ℕ → HF A) (k : ℕ) : Prop :=  b 0 = emptyHF ∧ ∀ i < k,    (∃ D, choice (b i) = some D ∧ c i ∈ elements D) ∧    step (b i) (c i) = some (b (i+1))def StrictPrefix (b : ℕ → HF A) (k : ℕ) : Prop := ∀ i < k, b i ≠ b (i+1)def FirstPath (step : HF A → HF A → Result (HF A))    (choice : HF A → Result (HF A)) (b c : ℕ → HF A) (t : ℕ) : Prop :=  ChoicePrefix step choice b c (t+1) ∧ StrictPrefix b t ∧ b t = b (t+1)def FixesParameters {n : ℕ} (free : Finset (Fin n)) (env : Fin n → HF A)    (g : Equiv.Perm A) : Prop := ∀ i ∈ free, g • env i = env idef WitnessesHistory {n : ℕ} (S : Input A) (free : Finset (Fin n))    (env : Fin n → HF A) (b : ℕ → HF A) (i : ℕ) (D M : HF A) : Prop :=  isSet M = true ∧  (∀ w ∈ elements M, ∃ g : Equiv.Perm A,    w = permutationGraph g ∧ Automorphism S g ∧ FixesParameters free env g ∧      ∀ j ≤ i, g • b j = b j) ∧  (∀ u ∈ elements D, ∀ v ∈ elements D, ∃ g : Equiv.Perm A,    permutationGraph g ∈ elements M ∧ g • u = v)def GoodWSC {n : ℕ} (S : Input A) (p : ℕ) (free : Finset (Fin n))    (env : Fin n → HF A) (step : HF A → HF A → Result (HF A))    (choice : HF A → Result (HF A)) (witness : HF A → HF A → Result (HF A))    (output : HF A → Result Bool) : Prop :=  (∀ b c k, ChoicePrefix step choice b c k → StrictPrefix b k →    k ≤ p ∧ (TC (b k)).card ≤ p ∧ ∃ D, choice (b k) = some D ∧      (elements D).Nonempty ∧ ∀ u ∈ elements D, (step (b k) u).isSome) ∧  (∀ b c t, FirstPath step choice b c t → t+2 ≤ p ∧    (∀ i ≤ t, ∃ D M, choice (b i) = some D ∧ witness (b t) (b i) = some M ∧      WitnessesHistory S free env b i D M) ∧ (output (b t)).isSome)def witnessedIteration {n : ℕ} (S : Input A) (p : ℕ) (free : Finset (Fin n))    (env : Fin n → HF A) (step : HF A → HF A → Result (HF A))    (choice : HF A → Result (HF A)) (witness : HF A → HF A → Result (HF A))    (output : HF A → Result Bool) : Result Bool :=  if GoodWSC S p free env step choice witness output then    some (decide (∀ b c t, FirstPath step choice b c t → output (b t) = some true))  else nonemutualdef Term.eval (S : Input A) (p : Polynomial ℝ) : {n : ℕ} → Term n →      (Fin n → HF A) → Result (HF A)    | _, .var i, env => some (env i)    | _, .empty, _ => some emptyHF    | _, .atoms, _ => some (ofFinset (Finset.univ.image atom))    | _, .pair a b, env => lift₂ double (a.eval S p env) (b.eval S p env)    | _, .union a, env => (a.eval S p env).map unionHF    | _, .unique a, env => (a.eval S p env).map uniqueHF    | _, .card a, env => (a.eval S p env).map cardHF    | _, .comprehend body range guard, env =>        (range.eval S p env).bind (fun r => collect r          (fun x => guard.eval S p (Fin.cons x env))          (fun x => body.eval S p (Fin.cons x env)))    | _, .iterate step, env => ordinaryIteration (resource p (Fintype.card A))        (fun x => step.eval S p (Fin.cons x env))  def Formula.eval (S : Input A) (p : Polynomial ℝ) : {n : ℕ} → Formula n →      (Fin n → HF A) → Result Bool    | _, .equal a b, env => lift₂ (fun x y => decide (x = y)) (a.eval S p env) (b.eval S p env)    | _, .input r a b, env => lift₂ (inputHF S r) (a.eval S p env) (b.eval S p env)    | _, .neg a, env => (a.eval S p env).map Bool.not    | _, .and a b, env => lift₂ Bool.and (a.eval S p env) (b.eval S p env)    | _, .or a b, env => lift₂ Bool.or (a.eval S p env) (b.eval S p env)    | _, .wsc step choice witness output, env =>        witnessedIteration S (resource p (Fintype.card A))          (Formula.wsc step choice witness output).free env          (fun x y => step.eval S p (Fin.cons y (Fin.cons x env)))          (fun x => choice.eval S p (Fin.cons x env))          (fun z x => witness.eval S p (Fin.cons x (Fin.cons z env)))          (fun x => output.eval S p (Fin.cons x env))endstructure FiniteInput where  Carrier : Type  finite : Fintype Carrier  input : Input Carrierattribute [instance] FiniteInput.finitestructure Sentence where  formula : Formula 0  polynomial : Polynomial ℝdef Sentence.eval (φ : Sentence) (S : FiniteInput) : Result Bool :=  φ.formula.eval S.input φ.polynomial Fin.elim0def Sentence.isCPT (φ : Sentence) : Prop := φ.formula.wscCount = 0def Sentence.BooleanOnAllInputs (φ : Sentence) : Prop :=  ∀ S, ∃ b : Bool, φ.eval S = some bdef Sentence.TrueModels (φ : Sentence) : Set FiniteInput := {S | φ.eval S = some true}def MainStatement : Prop := ∃ φ : Sentence,  φ.formula.wscCount = 1 ∧ φ.BooleanOnAllInputs ∧    ∀ ψ : Sentence, ψ.isCPT → φ.TrueModels ≠ ψ.TrueModelsend BGSend WitnessedChoicetheorem WitnessedChoice.main : WitnessedChoice.BGS.MainStatement := by  sorryendend 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

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.
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:

  1. (i)

    (\Phi,p) has a Boolean value on every finite \tau-structure;

  2. (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
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 243 link it.
Solution module
OAI.Computability.WitnessedChoice.Main
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
62 local vocabulary declarations
Lines of Lean, without comments or blank lines
357
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

Strict expressive gain from one witnessed symmetric choice

Family 243: Separating choiceless counting from polynomial time and witnessed choice

Candidate pairing

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:

  1. (i)

    (\Phi,p) has a Boolean value on every finite \tau-structure;

  2. (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.

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

TeX label thm:main, build/sections/00-introduction.tex, line 38

The Lean statement says

def MainStatement : Prop := ∃ φ : Sentence,  φ.formula.wscCount = 1 ∧ φ.BooleanOnAllInputs ∧    ∀ ψ : Sentence, ψ.isCPT → φ.TrueModels ≠ ψ.TrueModelstheorem WitnessedChoice.main : WitnessedChoice.BGS.MainStatement := 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.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.three independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

62 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/WitnessedChoice.html

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.

Compare this statement with the paperShare a Comparator run reportSuggest a change