Refuting two prime-counting conjectures

def pairSet (n : ℕ) : Set (ℕ × ℕ) :=
  {p | 0 < p.1 ∧ 0 < p.2 ∧
    n = Nat.primeCounting (p.1 * (p.1 + 1) / 2) +
      Nat.primeCounting (1 + p.2 * (p.2 + 1) / 2)}

noncomputable def a (n : ℕ) : ℕ := (pairSet n).ncard

theorem pairSet_241540 : pairSet 241540 = ∅

theorem a_241540 : a 241540 = 0

$$\pi (T_{2596})=241602,\pi (1+T_{2596})=241603.$$

Both are larger than $241540$. If $k\ge 2596$, then $T_k\ge T_{2596}$, so

$$\pi (T_k)+\pi (1+T_m)\ge \pi (T_k)\ge 241602>241540.$$

Such a pair cannot work. The same argument excludes $m\ge 2596$. Every possible representation must therefore satisfy

$$1\le k\le 2595,1\le m\le 2595.$$

The largest argument needed here is

$$1+T_{2596}=3370907<{1837}^2.$$

Thus primes below $1837$ suffice to sieve the required range. The implementation works in finite windows and proves that a surviving bit corresponds exactly to a prime. Counting those bits gives the number of primes in each interval. Adding the interval counts certifies the tables

$$A_k=\pi (T_k),B_m=\pi (1+T_m).$$

The listed table values are not assumptions: The source proves that its table checker returns correct prime counts and then evaluates the checks in Lean's kernel. The tables include indices through $2596$, covering every possible solution and the cutoff values used above.

Write $N=241540$. For a fixed value $b=B_m$, the equation we want to rule out is

$$A_k+b=N.$$

If $b>N$, it is impossible because $A_k\ge 0$. Otherwise it is equivalent to

$$A_k=N-b.$$

So instead of repeatedly adding every pair of table entries, we can ask whether the complement $N-b$ occurs anywhere in the first table.

The source records that first table as a bitmask: An integer whose bit at position $r$ is 1 exactly when $r$ occurs as an $A_k$ for a positive table index $k$. For example, a table containing $\{0,2,5\}$ would set bits 0, 2, and 5, giving

$$2^0+2^2+2^5=37.$$

Testing bit 2 would report a match; testing bit 3 would not. Repeated table values simply set the same bit again. That is enough here because we are testing existence, not counting how many indices produce each value.

For every positive-index entry $b$ in the second table, the check verifies either $b>N$ or that bit $N-b$ is unset. Every entry passes: No complement occurs. The source proves what the bitmask lookup means and uses decide +kernel to certify that the finite check returns true.

The bitmask makes the computation efficient; the bounds make it exhaustive. This is not merely a search that failed to find a pair. The bounds exclude every larger pair, and the certified calculation excludes every remaining pair. Thus

$$\boxed{a(241540)=0.}$$

def pairSet (n : ℕ) : Set (ℕ × ℕ) :=
  {p | 0 < p.1 ∧ 0 < p.2 ∧
    n = Nat.primeCounting (p.1 ^ 2) +
      Nat.primeCounting (p.2 ^ 2 / 2)}

noncomputable def a (n : ℕ) : ℕ := (pairSet n).ncard

theorem mem_pairSet_15293 (k m : ℕ) :
    (k, m) ∈ pairSet 15293 ↔ k = 339 ∧ m = 291

theorem a_15293 : a 15293 = 1

Division of natural numbers in Lean rounds down, so p.2 ^ 2 / 2 is $\lfloor m^2/2\rfloor$. The symbol ↔ means “if and only if”: A pair represents $15293$ exactly when its coordinates are $339$ and $291$.

First, that pair works:

$$\pi ({339}^2)=\pi (114921)=10867,$$ $$\pi (\lfloor {291}^2/2\rfloor )=\pi (42340)=4426,$$

and $10867+4426=15293$.

But finding one pair is not enough to prove uniqueness. We must rule out every other pair. As before, two certified prime counts give bounds:

$$\pi ({410}^2)=15346>15293,$$ $$\pi (\lfloor {579}^2/2\rfloor )=15308>15293.$$

If $k\ge 410$ or $m\ge 579$, one summand alone already exceeds the target. Every solution must therefore lie in

$$1\le k\le 409,1\le m\le 578.$$

The kernel-checked table calculation excludes every $k$ except $339$. For that value, the second summand must be $15293-10867=4426$. The table then shows that only $m=291$ gives that count.

There is exactly one representing pair, so

$$\boxed{a(15293)=1.}$$