Lean statement

QMA-hardness of continuum Coulomb energy with binary charges

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.

Theorems selected for verification: OAI.ContinuumCoulomb.unit_coulomb_qmaHard OAI.ContinuumCoulomb.binary_coulomb_qmaHard

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

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 unit_coulomb_qmaHard : QMAHard unitCoulombCodec.encode unitCoulombPromise := by  sorry⋮theorem binary_coulomb_qmaHard : QMAHard binaryCoulombCodec.encode binaryCoulombPromise := 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.ContinuumCoulomb.BinaryEncoding.BitString line 12
```
abbrev BitString := List Bool
```

structure OAI.ContinuumCoulomb.BinaryEncoding.Codec line 14

structure Codec (α : Type*) where  encode : α → BitString  read : BitString → α × BitString  read_encode : ∀ x tail, read (encode x ++ tail) = (x, tail)

definition OAI.ContinuumCoulomb.BinaryEncoding.encodeDigits line 19

def encodeDigits : BitString → BitString  | [] => [false]  | b :: bs => true :: b :: encodeDigits bs

definition OAI.ContinuumCoulomb.BinaryEncoding.readDigits line 23

def readDigits : BitString → BitString × BitString  | true :: b :: bs => let (digits, tail) := readDigits bs; (b :: digits, tail)  | false :: bs => ([], bs)  | _ => ([], [])

definition OAI.ContinuumCoulomb.BinaryEncoding.decodeDigits line 34

def decodeDigits : BitString → ℕ  | [] => 0  | b :: bs => Nat.bit b (decodeDigits bs)

definition OAI.ContinuumCoulomb.BinaryEncoding.natural line 43

def natural : Codec ℕ where  encode n := encodeDigits n.bits  read s := let (digits, tail) := readDigits s; (decodeDigits digits, tail)  read_encode n tail := by simp only [readDigits_encode, decodeDigits_bits]

definition OAI.ContinuumCoulomb.BinaryEncoding.encodeUnary line 48

def encodeUnary : ℕ → BitString  | 0 => [false]  | n + 1 => true :: encodeUnary n

definition OAI.ContinuumCoulomb.BinaryEncoding.readUnary line 52

def readUnary : BitString → ℕ × BitString  | true :: s => let (n, tail) := readUnary s; (n + 1, tail)  | false :: s => (0, s)  | [] => (0, [])

definition OAI.ContinuumCoulomb.BinaryEncoding.unary line 63

def unary : Codec ℕ where  encode := encodeUnary  read := readUnary  read_encode := readUnary_encode

definition OAI.ContinuumCoulomb.BinaryEncoding.integer line 68

def integer : Codec ℤ where  encode    | Int.ofNat n => false :: natural.encode n    | Int.negSucc n => true :: natural.encode n  read    | false :: s => let (n, tail) := natural.read s; (Int.ofNat n, tail)    | true :: s => let (n, tail) := natural.read s; (Int.negSucc n, tail)    | [] => (0, [])  read_encode z tail := by    cases z <;> simp only [List.cons_append, natural.read_encode]

definition OAI.ContinuumCoulomb.BinaryEncoding.pair line 79

def pair {α β : Type*} (a : Codec α) (b : Codec β) : Codec (α × β) where  encode x := a.encode x.1 ++ b.encode x.2  read s := let (x, t) := a.read s; let (y, u) := b.read t; ((x, y), u)  read_encode x tail := by    rcases x with ⟨x, y⟩    simp only [List.append_assoc, a.read_encode, b.read_encode]

definition OAI.ContinuumCoulomb.BinaryEncoding.readCount line 86

def readCount {α : Type*} (a : Codec α) : ℕ → BitString → List α × BitString  | 0, s => ([], s)  | n + 1, s => let (x, t) := a.read s; let (xs, u) := readCount a n t; (x :: xs, u)

definition OAI.ContinuumCoulomb.BinaryEncoding.list line 97

def list {α : Type*} (a : Codec α) : Codec (List α) where  encode xs := natural.encode xs.length ++ xs.flatMap a.encode  read s := let (n, t) := natural.read s; readCount a n t  read_encode xs tail := by    simp only [List.append_assoc, natural.read_encode, readCount_encode]

definition OAI.ContinuumCoulomb.BinaryEncoding.equiv line 103

def equiv {α β : Type*} (a : Codec α) (e : β ≃ α) : Codec β where  encode x := a.encode (e x)  read s := let (x, t) := a.read s; (e.symm x, t)  read_encode x tail := by simp only [a.read_encode, e.symm_apply_apply]

definition OAI.ContinuumCoulomb.BinaryEncoding.sum line 108

def sum {α β : Type*} (a : Codec α) (b : Codec β) : Codec (α ⊕ β) where  encode    | Sum.inl x => false :: a.encode x    | Sum.inr y => true :: b.encode y  read    | false :: s => let (x, t) := a.read s; (Sum.inl x, t)    | true :: s => let (y, t) := b.read s; (Sum.inr y, t)    | [] => let (x, t) := a.read []; (Sum.inl x, t)  read_encode x tail := by    cases x <;> simp only [List.cons_append, a.read_encode, b.read_encode]

abbreviation OAI.Coulomb.Space line 125

abbrev Space := EuclideanSpace ℝ (Fin 3)

abbreviation OAI.Coulomb.Configuration line 126

abbrev Configuration (n : ℕ) := EuclideanSpace ℝ (Fin n × Fin 3)

abbreviation OAI.Coulomb.Spins line 127

abbrev Spins (n : ℕ) := Fin n → Fin 2

structure OAI.Coulomb.Nuclei line 129

structure Nuclei (M : ℕ) where  nonempty : 0 < M  position : Fin M → Space  distinct : Function.Injective position  charge : Fin M → ℝ  charge_ge_one : ∀ j, 1 ≤ charge j

definition OAI.Coulomb.position line 136

noncomputable def position {n : ℕ} (x : Configuration n) (i : Fin n) : Space :=  WithLp.toLp 2 (fun b => x (i, b))

definition OAI.Coulomb.coulombKernel line 139

noncomputable def coulombKernel (x : Space) : ℝ := ‖x‖⁻¹

definition OAI.Coulomb.attraction line 141

noncomputable def attraction {M : ℕ} (S : Nuclei M) (x : Space) : ℝ :=  ∑ j, S.charge j * coulombKernel (x - S.position j)

definition OAI.Coulomb.permute line 144

noncomputable def permute {n : ℕ} (p : Equiv.Perm (Fin n))    (x : Configuration n) : Configuration n :=  WithLp.toLp 2 (fun ib => x (p ib.1, ib.2))

structure OAI.Coulomb.H1Vector line 148

structure H1Vector (n : ℕ) where  value : Spins n → Configuration n → ℂ  gradient : Spins n → (Fin n × Fin 3) → Configuration n → ℂ  value_L2 : ∀ s, MemLp (value s) 2 volume  partial_L2 : ∀ s a, MemLp (gradient s a) 2 volume  weak_partial : ∀ s a (φ : Configuration n → ℝ),    ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →      (∫ x, value s x * (fderiv ℝ φ x (EuclideanSpace.single a 1) : ℂ)) =        -(∫ x, gradient s a x * (φ x : ℂ))

58 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: distinct, unary, positions, data, electrons, lengths, coulomb, many and 13 more. Found in the paper’s title, which its main theorem states: energy. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: electronic, separation, produces, thresholds, output, hardness, least, reductions and one more.

Statements in QMA-hardness of continuum Coulomb energy with unit nuclear charges come first because the release’s name for this Lean statement shares words with that paper’s title.

Theorem 1 of QMA-hardness of continuum Coulomb energy with unit nuclear charges

Theorem (Unit-charge Coulomb hardness)

The electronic promise problem for (eq:electronic-H) on \mathcal H_N, with distinct rational nuclear positions, all nuclear charges equal to one, unary electron number, and rational thresholds separated by at least L^{-1}, is QMA-hard under deterministic classical polynomial-time many-one reductions. The reduction produces polynomially many nuclei and electrons, polynomial rational bit lengths, and threshold separation at least one. The only output data are the nuclear positions, electron number, and thresholds.

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

Show the TeX

The electronic promise problem for~\eqref{eq:electronic-H} on
$\mathcal H_N$, with distinct rational nuclear positions, all nuclear
charges equal to one, unary electron number, and rational thresholds
separated by at least $L^{-1}$, is QMA-hard under deterministic classical
polynomial-time many-one reductions. The reduction produces
polynomially many nuclei and electrons, polynomial rational bit lengths,
and threshold separation at least one. The only output data are the
nuclear positions, electron number, and thresholds.

Other possible paper matches, closest wording first

Theorem 1.1 of Continuum Coulomb hardness with binary nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: many, hard, promise, qma, time, one and one more. Found in the paper’s title, which its main theorem states: binary, coulomb, nuclear and charges. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: instances, produce, reductions and deterministic.
Proposition 5 of QMA-hardness of continuum Coulomb energy with unit nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: state, antisymmetric, lower, electron, spin, scale and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: sector and continuum.
Proposition 4 of QMA-hardness of continuum Coulomb energy with unit nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: 2/3, space, norm, function, energy, form and four more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: three.
Proposition 3 of QMA-hardness of continuum Coulomb energy with unit nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: last, control, norm, spin, scale, form and three more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: range.
Theorem 2.1 of Continuum Coulomb hardness with binary nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: complete, poly, lattice, qubit, signed, source and seven more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: separation and thresholds.
Proposition 6 of QMA-hardness of continuum Coulomb energy with unit nuclear charges. Words of the Lean statement, its names split into words, that also appear in the theorem: eq, energy, nuclei, scale, unit and polynomial. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: continuum.

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

Atlas has no report of an independent group using Comparator to verify OpenAI’s proof of this Lean statement at the version shown here. 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…

No verdict reached Their term: “REFUSED”.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
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.

Built; Comparator not run Their term: “closure-pass”.
The solution was built and its dependency closure checked; Comparator was not run.
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 275’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: unit_coulomb_qmaHard : QMAHard unitCoulombCodec.encode unitCoulombPromise and binary_coulomb_qmaHard: every promise problem in QMA (verifier circuits over {H, T, CNOT} generated by a Mathlib Turing.TM2ComputableInPolyTime, completeness 2/3, soundness 1/3) has a deterministic polynomial-time many-one reduction (PolynomialManyOne, also Mathlib TM2 poly-time) to deciding groundEnergy ≤ lower versus upper ≤ groundEnergy with 1 ≤ upper - lower, distinct rational nuclear positions, unary electron count and (for the unit version) unit charges; groundEnergy is the sInf over normalized antisymmetric H¹ states of the two-spin Coulomb form kinetic - nuclearEnergy + pairEnergy. External package RellichKondrachov is in the cone.
Definitions the group asks readers to compare with the paper: Custom complexity setup: hand-written QMAGate/QMACircuit/QuantumVerifier/InQMA (QMA over gate set {H, T, CNOT}, acceptance = Born probability of the last qubit being 1), PromiseProblem, QMAHard, and a Codec library for binary/unary encodings; polynomial time itself is Mathlib's Turing.TM2ComputableInPolyTime (not custom). groundEnergy is an EReal-valued sInf of Bochner-integral forms on H¹ vectors, which is fine because Hardy's inequality makes the Coulomb terms integrable.
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 QMA-hardness of approximating the electronic Coulomb spectral infimum in three-dimensional continuum space when positive integer nuclear charges are encoded in binary. The instances have distinct rational nuclear positions and a unary electron count, and the energy ranges over antisymmetric continuum states and all spin sectors. A deterministic polynomial-time many-one reduction produces the promise gap with threshold separation at least one, while keeping the complete output length polynomial. The same Comparator file also contains the companion unit-charge result.”
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

556 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: 300 to its own declarations, 214 to Mathlib’s documentation. 101 declared names also link to the same declaration in OpenAI’s library. 4 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 sectionopen MeasureTheoryopen scoped BigOperatorsnamespace ContinuumCoulomb.BinaryEncodingabbrev BitString := List Boolstructure Codec (α : Type*) where  encode : α → BitString  read : BitString → α × BitString  read_encode : ∀ x tail, read (encode x ++ tail) = (x, tail)def encodeDigits : BitString → BitString  | [] => [false]  | b :: bs => true :: b :: encodeDigits bsdef readDigits : BitString → BitString × BitString  | true :: b :: bs => let (digits, tail) := readDigits bs; (b :: digits, tail)  | false :: bs => ([], bs)  | _ => ([], [])theorem readDigits_encode (digits tail : BitString) :    readDigits (encodeDigits digits ++ tail) = (digits, tail) := by  induction digits with  | nil => rfl  | cons b digits ih => simp only [encodeDigits, List.cons_append, readDigits, ih]def decodeDigits : BitString → ℕ  | [] => 0  | b :: bs => Nat.bit b (decodeDigits bs)theorem decodeDigits_bits (n : ℕ) : decodeDigits n.bits = n := by  induction n using Nat.binaryRec' with  | zero => rfl  | bit b n h ih => simp only [Nat.bits_append_bit n b h, decodeDigits, ih]def natural : Codec ℕ where  encode n := encodeDigits n.bits  read s := let (digits, tail) := readDigits s; (decodeDigits digits, tail)  read_encode n tail := by simp only [readDigits_encode, decodeDigits_bits]def encodeUnary : ℕ → BitString  | 0 => [false]  | n + 1 => true :: encodeUnary ndef readUnary : BitString → ℕ × BitString  | true :: s => let (n, tail) := readUnary s; (n + 1, tail)  | false :: s => (0, s)  | [] => (0, [])theorem readUnary_encode (n : ℕ) (tail : BitString) :    readUnary (encodeUnary n ++ tail) = (n, tail) := by  induction n with  | zero => rfl  | succ n ih => simp only [encodeUnary, List.cons_append, readUnary, ih]def unary : Codec ℕ where  encode := encodeUnary  read := readUnary  read_encode := readUnary_encodedef integer : Codec ℤ where  encode    | Int.ofNat n => false :: natural.encode n    | Int.negSucc n => true :: natural.encode n  read    | false :: s => let (n, tail) := natural.read s; (Int.ofNat n, tail)    | true :: s => let (n, tail) := natural.read s; (Int.negSucc n, tail)    | [] => (0, [])  read_encode z tail := by    cases z <;> simp only [List.cons_append, natural.read_encode]def pair {α β : Type*} (a : Codec α) (b : Codec β) : Codec (α × β) where  encode x := a.encode x.1 ++ b.encode x.2  read s := let (x, t) := a.read s; let (y, u) := b.read t; ((x, y), u)  read_encode x tail := by    rcases x with ⟨x, y⟩    simp only [List.append_assoc, a.read_encode, b.read_encode]def readCount {α : Type*} (a : Codec α) : ℕ → BitString → List α × BitString  | 0, s => ([], s)  | n + 1, s => let (x, t) := a.read s; let (xs, u) := readCount a n t; (x :: xs, u)theorem readCount_encode {α : Type*} (a : Codec α) (xs : List α) (tail : BitString) :    readCount a xs.length (xs.flatMap a.encode ++ tail) = (xs, tail) := by  induction xs with  | nil => rfl  | cons x xs ih =>    simp only [List.length_cons, List.flatMap_cons, List.append_assoc, readCount, a.read_encode, ih]def list {α : Type*} (a : Codec α) : Codec (List α) where  encode xs := natural.encode xs.length ++ xs.flatMap a.encode  read s := let (n, t) := natural.read s; readCount a n t  read_encode xs tail := by    simp only [List.append_assoc, natural.read_encode, readCount_encode]def equiv {α β : Type*} (a : Codec α) (e : β ≃ α) : Codec β where  encode x := a.encode (e x)  read s := let (x, t) := a.read s; (e.symm x, t)  read_encode x tail := by simp only [a.read_encode, e.symm_apply_apply]def sum {α β : Type*} (a : Codec α) (b : Codec β) : Codec (α ⊕ β) where  encode    | Sum.inl x => false :: a.encode x    | Sum.inr y => true :: b.encode y  read    | false :: s => let (x, t) := a.read s; (Sum.inl x, t)    | true :: s => let (y, t) := b.read s; (Sum.inr y, t)    | [] => let (x, t) := a.read []; (Sum.inl x, t)  read_encode x tail := by    cases x <;> simp only [List.cons_append, a.read_encode, b.read_encode]end ContinuumCoulomb.BinaryEncodingnamespace Coulombopen scoped ENNReal Classical NNReal ComplexConjugateabbrev Space := EuclideanSpace ℝ (Fin 3)abbrev Configuration (n : ℕ) := EuclideanSpace ℝ (Fin n × Fin 3)abbrev Spins (n : ℕ) := Fin n → Fin 2structure Nuclei (M : ℕ) where  nonempty : 0 < M  position : Fin M → Space  distinct : Function.Injective position  charge : Fin M → ℝ  charge_ge_one : ∀ j, 1 ≤ charge jnoncomputable def position {n : ℕ} (x : Configuration n) (i : Fin n) : Space :=  WithLp.toLp 2 (fun b => x (i, b))noncomputable def coulombKernel (x : Space) : ℝ := ‖x‖⁻¹noncomputable def attraction {M : ℕ} (S : Nuclei M) (x : Space) : ℝ :=  ∑ j, S.charge j * coulombKernel (x - S.position j)noncomputable def permute {n : ℕ} (p : Equiv.Perm (Fin n))    (x : Configuration n) : Configuration n :=  WithLp.toLp 2 (fun ib => x (p ib.1, ib.2))structure H1Vector (n : ℕ) where  value : Spins n → Configuration n → ℂ  gradient : Spins n → (Fin n × Fin 3) → Configuration n → ℂ  value_L2 : ∀ s, MemLp (value s) 2 volume  partial_L2 : ∀ s a, MemLp (gradient s a) 2 volume  weak_partial : ∀ s a (φ : Configuration n → ℝ),    ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →      (∫ x, value s x * (fderiv ℝ φ x (EuclideanSpace.single a 1) : ℂ)) =        -(∫ x, gradient s a x * (φ x : ℂ))def Antisymmetric {n : ℕ} (ψ : H1Vector n) : Prop :=  ∀ (p : Equiv.Perm (Fin n)) (s : Spins n),    ∀ᵐ x ∂volume,      ψ.value (s ∘ p) (permute p x) = ((p.sign : ℤ) : ℂ) * ψ.value s xnoncomputable def mass {n : ℕ} (ψ : H1Vector n) : ℝ :=  ∑ s, ∫ x, ‖ψ.value s x‖ ^ 2noncomputable def kinetic {n : ℕ} (ψ : H1Vector n) : ℝ :=  (1 / 2 : ℝ) * ∑ s, ∑ a, ∫ x, ‖ψ.gradient s a x‖ ^ 2noncomputable def nuclearEnergy {M n : ℕ} (S : Nuclei M) (ψ : H1Vector n) : ℝ :=  ∑ s, ∫ x, (∑ i, attraction S (position x i)) * ‖ψ.value s x‖ ^ 2noncomputable def pairEnergy {n : ℕ} (ψ : H1Vector n) : ℝ :=  ∑ s, ∫ x, (∑ i : Fin n, ∑ j : Fin n,    if i < j then coulombKernel (position x i - position x j) else 0) *      ‖ψ.value s x‖ ^ 2noncomputable def form {M n : ℕ} (S : Nuclei M) (ψ : H1Vector n) : ℝ :=  kinetic ψ - nuclearEnergy S ψ + pairEnergy ψend Coulombnamespace ContinuumCoulombopen BinaryEncoding Matrixopen scoped Kroneckerabbrev SourceSpinBasis (n : ℕ) := Fin n → Fin 2def sourceTensor (n : ℕ) (M : Fin n → Matrix (Fin 2) (Fin 2) ℂ) :    Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ := fun s t => ∏ i, M i (s i) (t i)sectiontheorem bellScale_atLeastTwo : Nat.AtLeastTwo (1 + 1) :=  @Nat.instAtLeastTwoHAddOfNat 1 (@Nat.instNeZeroSucc 0)attribute [local instance] bellScale_atLeastTwodef bellScale : ℂ := (Real.sqrt (1 / 2 : ℝ) : ℂ)endinductive QMAGate where  | hadamard (qubit : ℕ)  | phaseT (qubit : ℕ)  | controlledNot (control target : ℕ)  deriving DecidableEq, Reprdef qmaGateEquiv : QMAGate ≃ ((ℕ ⊕ ℕ) ⊕ (ℕ × ℕ)) where  toFun    | .hadamard i => Sum.inl (Sum.inl i)    | .phaseT i => Sum.inl (Sum.inr i)    | .controlledNot i j => Sum.inr (i, j)  invFun    | Sum.inl (Sum.inl i) => .hadamard i    | Sum.inl (Sum.inr i) => .phaseT i    | Sum.inr (i, j) => .controlledNot i j  left_inv g := by cases g <;> rfl  right_inv g := by rcases g with (i | i) | ⟨i, j⟩ <;> rfldef qmaGateCodec : Codec QMAGate := BinaryEncoding.equiv  (BinaryEncoding.sum (BinaryEncoding.sum natural natural) (pair natural natural)) qmaGateEquivstructure QMACircuit where  work : ℕ  witness : ℕ  gates : List QMAGate  deriving DecidableEq, Reprdef qmaCircuitEquiv : QMACircuit ≃ (ℕ × (ℕ × List QMAGate)) where  toFun c := (c.work, c.witness, c.gates)  invFun c := ⟨c.1, c.2.1, c.2.2⟩  left_inv c := by cases c; rfl  right_inv c := by rcases c with ⟨n, w, gs⟩; rfldef qmaCircuitCodec : Codec QMACircuit := BinaryEncoding.equiv  (pair natural (pair natural (BinaryEncoding.list qmaGateCodec))) qmaCircuitEquivdef QMAGate.WellFormed (n : ℕ) : QMAGate → Prop  | .hadamard i => i < n  | .phaseT i => i < n  | .controlledNot i j => i < n ∧ j < n ∧ i ≠ jdef QMACircuit.WellFormed (c : QMACircuit) : Prop :=  c.witness ≤ c.work ∧ ∀ g ∈ c.gates, g.WellFormed (c.work + 1)def qmaHadamard : Matrix (Fin 2) (Fin 2) ℂ :=  bellScale • !![1, 1; 1, -1]def qmaPhaseT : Matrix (Fin 2) (Fin 2) ℂ :=  !![1, 0; 0, bellScale * (1 + Complex.I)]def qmaQubit (work index : ℕ) : Fin (work + 1) :=  ⟨index % (work + 1), Nat.mod_lt _ (Nat.succ_pos _)⟩def qmaControlledNot (work : ℕ) (control target : Fin (work + 1))    (s : SourceSpinBasis (work + 1)) : SourceSpinBasis (work + 1) :=  fun i => if i = target ∧ s control = 1 then Equiv.swap (0 : Fin 2) 1 (s i) else s idef qmaGateMatrix (work : ℕ) : QMAGate →    Matrix (SourceSpinBasis (work + 1)) (SourceSpinBasis (work + 1)) ℂ  | .hadamard i => sourceTensor (work + 1)      (fun k => if k = qmaQubit work i then qmaHadamard else 1)  | .phaseT i => sourceTensor (work + 1)      (fun k => if k = qmaQubit work i then qmaPhaseT else 1)  | .controlledNot i j => fun s t =>      if s = qmaControlledNot work (qmaQubit work i) (qmaQubit work j) t then 1 else 0def qmaCircuitMatrix (c : QMACircuit) :    Matrix (SourceSpinBasis (c.work + 1)) (SourceSpinBasis (c.work + 1)) ℂ :=  c.gates.foldl (fun M g => qmaGateMatrix c.work g * M) 1def qmaInitialState (c : QMACircuit) (hc : c.WellFormed)    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) :    SourceSpinBasis (c.work + 1) → ℂ :=  fun s => if ∀ i : Fin (c.work + 1), c.witness ≤ i.val → s i = 0 then    psi (fun i => s ⟨i.val, lt_of_lt_of_le i.isLt (hc.1.trans (Nat.le_succ _))⟩)  else 0def qmaAcceptance (c : QMACircuit) (hc : c.WellFormed)    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) : ℝ :=  ∑ s : SourceSpinBasis (c.work + 1),    if s (Fin.last c.work) = 1 then      Complex.normSq ((qmaCircuitMatrix c).mulVec (qmaInitialState c hc psi) s) else 0structure QuantumVerifier where  generate : BitString → QMACircuit  uniform : Turing.TM2ComputableInPolyTime id qmaCircuitCodec.encode generate  size : Polynomial ℕ  size_bound : ∀ x, (generate x).work + (generate x).gates.length ≤ size.eval x.length  wellFormed : ∀ x, (generate x).WellFormedstructure PromiseProblem (α : Type) where  yes : Set α  no : Set α  disjoint : @Disjoint (Set α)    (@ChainCompletePartialOrder.toPartialOrder (Set α)      (@ChainCompletePartialOrder.instOfCompleteLattice (Set α)        (@CompleteBooleanAlgebra.toCompleteLattice (Set α)          (@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra (Set α)            (@Set.instCompleteAtomicBooleanAlgebra α)))))    (@HeytingAlgebra.toOrderBot (Set α)      (@Order.Frame.toHeytingAlgebra (Set α)        (@CompleteDistribLattice.toFrame (Set α)          (@CompleteBooleanAlgebra.toCompleteDistribLattice (Set α)            (@CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra (Set α)              (@Set.instCompleteAtomicBooleanAlgebra α))))))    yes nosectiontheorem inQMA_two_atLeastTwo : Nat.AtLeastTwo (1 + 1) :=  @Nat.instAtLeastTwoHAddOfNat 1 (@Nat.instNeZeroSucc 0)theorem inQMA_three_atLeastTwo : Nat.AtLeastTwo (2 + 1) :=  @Nat.instAtLeastTwoHAddOfNat 2 (@Nat.instNeZeroSucc 1)attribute [local instance] inQMA_two_atLeastTwo inQMA_three_atLeastTwodef InQMA (P : PromiseProblem BitString) : Prop :=  ∃ V : QuantumVerifier,    (∀ x ∈ P.yes, ∃ psi : EuclideanSpace ℂ (SourceSpinBasis (V.generate x).witness),      ‖psi‖ = 1 ∧ 2 / 3 ≤ qmaAcceptance (V.generate x) (V.wellFormed x) psi) ∧    (∀ x ∈ P.no, ∀ psi : EuclideanSpace ℂ (SourceSpinBasis (V.generate x).witness),      ‖psi‖ = 1 → qmaAcceptance (V.generate x) (V.wellFormed x) psi ≤ 1 / 3)endstructure PolynomialManyOne {α β : Type} (ea : α → BitString) (eb : β → BitString)    (P : PromiseProblem α) (Q : PromiseProblem β) where  map : α → β  polynomialTime : Turing.TM2ComputableInPolyTime ea eb map  maps_yes : ∀ x ∈ P.yes, map x ∈ Q.yes  maps_no : ∀ x ∈ P.no, map x ∈ Q.nodef QMAHard {α : Type} (encoding : α → BitString) (Q : PromiseProblem α) : Prop :=  ∀ P : PromiseProblem BitString, InQMA P → Nonempty (PolynomialManyOne id encoding P Q)structure BinaryRational where  numerator : ℤ  denominator : ℕ  deriving DecidableEq, Reprdef BinaryRational.value (q : BinaryRational) : ℚ :=  (q.numerator : ℚ) / q.denominatordef binaryRationalEquiv : BinaryRational ≃ (ℤ × ℕ) where  toFun q := (q.numerator, q.denominator)  invFun q := ⟨q.1, q.2⟩  left_inv q := by cases q; rfl  right_inv q := by cases q; rfldef binaryRationalCodec : Codec BinaryRational := BinaryEncoding.equiv (pair integer natural) binaryRationalEquivabbrev Position := Coulomb.Spaceabbrev Configuration := Coulomb.Configurationabbrev SpinConfiguration := Coulomb.Spinsstructure NuclearData where  nuclei : ℕ  nuclei_pos : 0 < nuclei  position : Fin nuclei → Fin 3 → ℚ  distinct : Function.Injective position  charge : Fin nuclei → ℕ  charge_pos : ∀ a, 0 < charge a  electrons : ℕ  electrons_pos : 0 < electronsstructure UnitNuclearData where  nuclei : ℕ  nuclei_pos : 0 < nuclei  position : Fin nuclei → Fin 3 → ℚ  distinct : Function.Injective position  electrons : ℕ  electrons_pos : 0 < electronsdef UnitNuclearData.toNuclearData (d : UnitNuclearData) : NuclearData where  nuclei := d.nuclei  nuclei_pos := d.nuclei_pos  position := d.position  distinct := d.distinct  charge := fun _ => 1  charge_pos := fun _ => Nat.zero_lt_one  electrons := d.electrons  electrons_pos := d.electrons_possectiontheorem realPosition_atLeastTwo : Nat.AtLeastTwo (1 + 1) :=  @Nat.instAtLeastTwoHAddOfNat 1 (@Nat.instNeZeroSucc 0)attribute [local instance] realPosition_atLeastTwodef realPosition (r : Fin 3 → ℚ) : Position :=  WithLp.toLp 2 (fun a => (r a : ℝ))endtheorem realPosition_injective : Function.Injective realPosition := by  intro r s hrs  funext a  have h := congrArg (fun p : Position => p a) hrs  change (r a : ℝ) = (s a : ℝ) at h  exact_mod_cast hdef NuclearData.toNuclei (d : NuclearData) : Coulomb.Nuclei d.nuclei where  nonempty := d.nuclei_pos  position := fun a => realPosition (d.position a)  distinct := realPosition_injective.comp d.distinct  charge := fun a => (d.charge a : ℝ)  charge_ge_one := by    intro a    exact_mod_cast d.charge_pos aabbrev FormState (n : ℕ) := {state : Coulomb.H1Vector n // Coulomb.Antisymmetric state}abbrev normSq {n : ℕ} (state : FormState n) := Coulomb.mass state.valabbrev kineticEnergy {n : ℕ} (state : FormState n) := Coulomb.kinetic state.valdef coulombForm (d : NuclearData) (state : FormState d.electrons) : ℝ :=  Coulomb.form d.toNuclei state.valdef unitCoulombForm (d : UnitNuclearData) (state : FormState d.electrons) : ℝ :=  coulombForm d.toNuclearData statedef groundEnergy (d : NuclearData) : EReal :=  sInf {e | ∃ state : FormState d.electrons,    normSq state = 1 ∧ e = (coulombForm d state : EReal)}def unitGroundEnergy (d : UnitNuclearData) : EReal :=  sInf {e | ∃ state : FormState d.electrons,    normSq state = 1 ∧ e = (unitCoulombForm d state : EReal)}structure BinaryPosition where  x : BinaryRational  y : BinaryRational  z : BinaryRational  deriving DecidableEq, Reprdef BinaryPosition.value (p : BinaryPosition) : Fin 3 → ℚ := ![p.x.value, p.y.value, p.z.value]def BinaryPosition.Valid (p : BinaryPosition) : Prop :=  0 < p.x.denominator ∧ 0 < p.y.denominator ∧ 0 < p.z.denominatordef binaryPositionEquiv : BinaryPosition ≃ (BinaryRational × (BinaryRational × BinaryRational)) where  toFun p := (p.x, p.y, p.z)  invFun p := ⟨p.1, p.2.1, p.2.2⟩  left_inv p := by cases p; rfl  right_inv p := by rcases p with ⟨x, y, z⟩; rfldef binaryPositionCodec : Codec BinaryPosition := BinaryEncoding.equiv  (pair binaryRationalCodec (pair binaryRationalCodec binaryRationalCodec)) binaryPositionEquivstructure BinaryCoulomb where  nuclei : List (BinaryPosition × ℕ)  electrons : ℕ  lower : BinaryRational  upper : BinaryRational  deriving DecidableEq, Reprdef binaryCoulombEquiv : BinaryCoulomb ≃    (List (BinaryPosition × ℕ) × (ℕ × (BinaryRational × BinaryRational))) where  toFun d := (d.nuclei, d.electrons, d.lower, d.upper)  invFun d := ⟨d.1, d.2.1, d.2.2.1, d.2.2.2⟩  left_inv d := by cases d; rfl  right_inv d := by rcases d with ⟨ns, n, a, b⟩; rfldef binaryCoulombCodec : Codec BinaryCoulomb := BinaryEncoding.equiv  (pair (BinaryEncoding.list (pair binaryPositionCodec natural))    (pair unary (pair binaryRationalCodec binaryRationalCodec))) binaryCoulombEquivstructure BinaryCoulomb.Valid (d : BinaryCoulomb) : Prop where  nuclei_pos : 0 < d.nuclei.length  electrons_pos : 0 < d.electrons  positions : ∀ a : Fin d.nuclei.length, (d.nuclei.get a).1.Valid  distinct : Function.Injective (fun a : Fin d.nuclei.length => (d.nuclei.get a).1.value)  charge_pos : ∀ a : Fin d.nuclei.length, 0 < (d.nuclei.get a).2  lower_denominator : 0 < d.lower.denominator  upper_denominator : 0 < d.upper.denominator  gap : 1 ≤ d.upper.value - d.lower.valuedef BinaryCoulomb.toData (d : BinaryCoulomb) (h : d.Valid) : NuclearData where  nuclei := d.nuclei.length  nuclei_pos := h.nuclei_pos  position a := (d.nuclei.get a).1.value  distinct := h.distinct  charge a := (d.nuclei.get a).2  charge_pos := h.charge_pos  electrons := d.electrons  electrons_pos := h.electrons_posstructure UnitCoulomb where  nuclei : List BinaryPosition  electrons : ℕ  lower : BinaryRational  upper : BinaryRational  deriving DecidableEq, Reprdef unitCoulombEquiv : UnitCoulomb ≃ (List BinaryPosition × (ℕ × (BinaryRational × BinaryRational))) where  toFun d := (d.nuclei, d.electrons, d.lower, d.upper)  invFun d := ⟨d.1, d.2.1, d.2.2.1, d.2.2.2⟩  left_inv d := by cases d; rfl  right_inv d := by rcases d with ⟨ns, n, a, b⟩; rfldef unitCoulombCodec : Codec UnitCoulomb := BinaryEncoding.equiv  (pair (BinaryEncoding.list binaryPositionCodec)    (pair unary (pair binaryRationalCodec binaryRationalCodec))) unitCoulombEquivstructure UnitCoulomb.Valid (d : UnitCoulomb) : Prop where  nuclei_pos : 0 < d.nuclei.length  electrons_pos : 0 < d.electrons  positions : ∀ a : Fin d.nuclei.length, (d.nuclei.get a).Valid  distinct : Function.Injective (fun a : Fin d.nuclei.length => (d.nuclei.get a).value)  lower_denominator : 0 < d.lower.denominator  upper_denominator : 0 < d.upper.denominator  gap : 1 ≤ d.upper.value - d.lower.valuedef UnitCoulomb.toData (d : UnitCoulomb) (h : d.Valid) : UnitNuclearData where  nuclei := d.nuclei.length  nuclei_pos := h.nuclei_pos  position a := (d.nuclei.get a).value  distinct := h.distinct  electrons := d.electrons  electrons_pos := h.electrons_posdef binaryCoulombPromise : PromiseProblem BinaryCoulomb where  yes := {d | ∃ h : d.Valid, groundEnergy (d.toData h) ≤ ((d.lower.value : ℝ) : EReal)}  no := {d | ∃ h : d.Valid, ((d.upper.value : ℝ) : EReal) ≤ groundEnergy (d.toData h)}  disjoint := by    apply Set.disjoint_left.mpr    rintro d ⟨h, hyes⟩ ⟨h', hno⟩    have hgap : d.lower.value < d.upper.value := by linarith [h.gap]    have hgap' : ((d.lower.value : ℝ) : EReal) < ((d.upper.value : ℝ) : EReal) := by exact_mod_cast hgap    exact (not_le_of_gt hgap') (hno.trans hyes)def unitCoulombPromise : PromiseProblem UnitCoulomb where  yes := {d | ∃ h : d.Valid, unitGroundEnergy (d.toData h) ≤ ((d.lower.value : ℝ) : EReal)}  no := {d | ∃ h : d.Valid, ((d.upper.value : ℝ) : EReal) ≤ unitGroundEnergy (d.toData h)}  disjoint := by    apply Set.disjoint_left.mpr    rintro d ⟨h, hyes⟩ ⟨h', hno⟩    have hgap : d.lower.value < d.upper.value := by linarith [h.gap]    have hgap' : ((d.lower.value : ℝ) : EReal) < ((d.upper.value : ℝ) : EReal) := by exact_mod_cast hgap    exact (not_le_of_gt hgap') (hno.trans hyes)theorem unit_coulomb_qmaHard : QMAHard unitCoulombCodec.encode unitCoulombPromise := by  sorrytheorem binary_coulomb_qmaHard : QMAHard binaryCoulombCodec.encode binaryCoulombPromise := by  sorryend ContinuumCoulombendend 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.

Continuum Coulomb hardness with binary nuclear charges

Theorem

The promise problem above is QMA-hard under deterministic classical polynomial-time many-one reductions for c=1. The reduction can produce instances with b-a\ge1.

Section 1, The problem and the result Read it in the paper TeX source, line 51

Show the TeX

The promise problem above is QMA-hard under deterministic classical polynomial-time many-one reductions for $c=1$. The reduction can produce instances with $b-a\ge1$.

QMA-hardness of continuum Coulomb energy with unit nuclear charges

Theorem (Unit-charge Coulomb hardness)

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

Show the TeX

The electronic promise problem for~\eqref{eq:electronic-H} on
$\mathcal H_N$, with distinct rational nuclear positions, all nuclear
charges equal to one, unary electron number, and rational thresholds
separated by at least $L^{-1}$, is QMA-hard under deterministic classical
polynomial-time many-one reductions. The reduction produces
polynomially many nuclei and electrons, polynomial rational bit lengths,
and threshold separation at least one. The only output data are the
nuclear positions, electron number, and thresholds.

Configuration and file facts

File: lean/ComparatorChallenges/ContinuumCoulombHardness.lean
OpenAI’s Lean catalogue: OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 275 link it.
Solution module: OAI.MathematicalPhysics.ContinuumCoulomb.Reduction.Hardness
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: 90 local vocabulary declarations
Lines of Lean, without comments or blank lines: 416
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