The claim

View on GitHub · Open in Lean playground (current Mathlib) · Inspect this claim on comparator.live

≈/-
Copyright (c) 2026 Eric Vergo. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Vergo, Claude Fable 5 (Claude Code)
-/
import Mathlib.Data.Nat.Nth
import Mathlib.NumberTheory.Real.Irrational

/-!
# Comparator challenge: the A362583 claim, stated independently

This module is the **comparator challenge**: an independent, auditable
statement of exactly what this project claims to prove.  It intentionally
imports nothing from the `A362583` library — the three definitions are copied
verbatim from `A362583/Defs.lean` and the main theorem statement from
`A362583/Main.lean`, here left with proof `sorry`.

The `sorry` is **by design**: this file is the comparator's *input*, not part of
any proof.  Its companion, the `Solution` module (`comparator/Solution.lean`),
re-states the same definitions and *proves* this theorem, deriving it from the
library's `A362583.irrational_ϱ`.  The comparator (`leanprover/comparator`;
Linux-only, run in CI — see `comparator.json` and `comparator-status.json`)
elaborates this challenge module and the `Solution` module in separate
environments and certifies, kernel-checked, that the solution proves this exact
statement — `Challenge.irrational_ϱ` — using only the permitted axioms
`propext`, `Classical.choice`, `Quot.sound`.
-/

namespace`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
  full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
  are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
  opening the namespace.

As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.

`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
 Challenge

/-- The `k`-th odd prime: `oddPrime 0 = 3`, `oddPrime 1 = 5`, `oddPrime 2 = 7`, ….
Writing the odd primes as `p_1, p_2, …`, this is `p_{k+1}`; since
`Nat.nth Nat.Prime 0 = 2`, skipping index 0 skips exactly the prime 2. -/
noncomputable def oddPrime (k : ℕ) : ℕ := Nat.nth Nat.Prime (k + 1)

/-- `k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`.
The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1`
(primes `3, 5, 7, 11, 13, 17, 19, 23`). -/
noncomputable def bit (k : ℕ) : ℕ := if`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 oddPrime k % 4 = 3 then`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 1 else`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 0

/-- The prime race constant (the A362583 constant): the sum of the series
`ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is
`bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the
successive digit prefixes read as binary integers. -/
noncomputable def ϱ : ℝ := ∑' k : ℕ, (bit k : ℝ) / 2 ^ (k + 1)

/-- **Primary deliverable**: the prime race constant `ϱ = Σ_{k ≥ 0} bₖ · 2^{-(k+1)}` (the
A362583 constant) — the number whose binary expansion is `0.b₀b₁b₂…₂`, where `bₖ = 1` iff
the `k`-th odd prime is `≡ 3 (mod 4)` — is irrational. -/
theorem irrational_ϱ : Irrational ϱ := sorryThe `sorry` term is a temporary placeholder for a missing proof or value.

The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.

"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.

Each `sorry` is guaranteed to be unique, so for example the following fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```

See also the `sorry` tactic, which is short for `exact sorry`.


end`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
 Challenge

comparator.live is experimental infrastructure run by the Lean FRO. The link pre-fills this exact challenge and solution in a live Lean and Mathlib environment, so both sources can be read and edited in the browser. It does not re-run the verdict: the solution imports this project's library, which comparator.live does not provide, so the pair check there stops at that import. Full verification is the CI run linked above and the local steps below.

What this page certifies

The statement comparator is an independent checking tool maintained by the Lean project. It elaborates the challenge and the solution in separate environments, so the solution cannot weaken or restate the claims it is measured against, and then asks the Lean kernel — and, independently, the nanoda kernel, a separate reimplementation of Lean's type checker — to confirm that the solution proves exactly the challenge statements, using only the permitted axioms listed above.

What you must still check yourself

One step is not automatable, and the comparator does not attempt it: reading the claim. The formal statement (reproduced in full above) must say what you take it to say, and its imports must bring in nothing beyond a library you already trust — here, Mathlib. A statement that quietly assumes its own conclusion, or that pulls in an axiom-bearing helper, would still pass the comparator.

About the statement comparator · Validating proofs (Lean reference) · Trust model and limitations

Reproduce it yourself

1. Open the challenge in the Lean playground — a zero-install check that the claim elaborates against the playground's current Mathlib. This checks the challenge statement only, not its comparison against the solution.
2. The CI verification record — the exact run that produced this verdict, Lean-kernel and nanoda replays included.
3. Run the check locally from a clean working directory:

   git clone https://github.com/eric-vergo/OEIS-A362583-Irrationality
   git clone --branch v4.32.0 https://github.com/leanprover/comparator.git comparator-tool
   (cd comparator-tool && git checkout 07bc4ea40f2266dcb861820a2ec1fa3244ed307f)
   (cd comparator-tool && lake build lean4export comparator)
   git clone https://github.com/ammkrn/nanoda_lib.git
   (cd nanoda_lib && git checkout f58f2f6d535e189a40fcb02ede8eb95f97a92d37)
   (cd nanoda_lib && cargo build --release --locked)
   cd OEIS-A362583-Irrationality
   COMPARATOR_NANODA=../nanoda_lib/target/release/nanoda_bin lake env ../comparator-tool/.lake/build/bin/comparator comparator/comparator.json

   CI additionally confines the solution in a Landlock sandbox (landrun 5ed4a3db3a4ad930d577215c6b9abaa19df7f99f). To match it on Linux, install landrun at that revision first — go install github.com/Zouuup/landrun/cmd/landrun@5ed4a3db3a4ad930d577215c6b9abaa19df7f99f — and re-run under it. Without that step, and always on macOS, the local run is a kernel check without the sandbox: weaker than what CI performed.

Solution (Lean)

View on GitHub

≈/-
Copyright (c) 2026 Eric Vergo. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Vergo, Claude Fable 5 (Claude Code)
-/
import A362583

/-!
# Comparator solution: proving the challenge statement

This module is the **official solution** to the comparator challenge
(`comparator/Challenge.lean`).  It re-states the three definitions verbatim and
*proves* the challenge theorem `Challenge.irrational_ϱ`, deriving it from the
`A362583` library's `A362583.irrational_ϱ`.

The comparator (`leanprover/comparator`; see `comparator.json`) loads this
module and the challenge module in **separate** environments, so this file must
not import `Challenge`: the three definitions below are byte-identical copies of
the challenge's (and hence of `A362583/Defs.lean`).  That makes each
`Challenge.*` constant definitionally identical across the two environments, so
the comparator can confirm statement equality and kernel-replay the proof.
-/

namespace`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
  full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
  are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
  opening the namespace.

As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.

`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
 Challenge

/-- The `k`-th odd prime: `oddPrime 0 = 3`, `oddPrime 1 = 5`, `oddPrime 2 = 7`, ….
Writing the odd primes as `p_1, p_2, …`, this is `p_{k+1}`; since
`Nat.nth Nat.Prime 0 = 2`, skipping index 0 skips exactly the prime 2. -/
noncomputable def oddPrime (k : ℕ) : ℕ := Nat.nth Nat.Prime (k + 1)

/-- `k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`.
The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1`
(primes `3, 5, 7, 11, 13, 17, 19, 23`). -/
noncomputable def bit (k : ℕ) : ℕ := if`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 oddPrime k % 4 = 3 then`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 1 else`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 0

/-- The prime race constant (the A362583 constant): the sum of the series
`ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is
`bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the
successive digit prefixes read as binary integers. -/
noncomputable def ϱ : ℝ := ∑' k : ℕ, (bit k : ℝ) / 2 ^ (k + 1)

/-- The challenge's constant is the library's `A362583.ϱ`: the two are
definitionally equal because the `oddPrime`, `bit`, `ϱ` definitions above are
byte-identical copies of the library's. -/
theorem ϱ_eq : ϱ = A362583.ϱ := rfl

/-- **Solution to the comparator challenge**: the challenge statement
`Irrational Challenge.ϱ`, proved by transporting the library's
`A362583.irrational_ϱ` across `ϱ_eq`. -/
theorem irrational_ϱ : Irrational ϱ := ϱ_eq ▸ A362583.irrational_ϱ

end`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
 Challenge

Comparator configuration

View config on GitHub

≈{"theorem_names": ["Challenge.irrational_ϱ"],
 "solution_module": "Solution",
 "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
 "enable_nanoda": true,
 "challenge_module": "Challenge"}