Review

Produced the exact reconstructed 7,194-point Sidon witness for {0,1}^24.

finding.add · pending

There exists a Sidon subset of {0,1}^24 with at least 7,193 elements.

finding.add · pending

Permit only the exact frozen Sidon 7,193-point witness workflow bound to the registered packet, producer profile, verifier capsule, positive result contract, and exact replay; all other work defers.

governance.policy_head · signed event

There exists a Sidon subset of {0,1}^24 with at least 7,193 elements.

finding.add · pending

The frozen Lean 4.27.0 capsule elaborates the exact theorem Erdos505.erdos_505.test_dim_one from this proof term and reports only propext, Classical.choice, and Quot.sound, with no sorryAx.

finding.add · pending

Exhaustive registered search over primes in 10428401..10428600 completed with a bounded negative result; the maximum factorial-residue fiber multiplicity found was 12 at p=10428581, residue=5141590.

finding.add · pending

Constructed an explicit nine-generator stabilizer witness for quantum:[[10,1,4]] and verified locally that the generators are distinct, non-identity, pairwise symplectically commuting, GF(2)-independent of rank nine, and that all 3,675 Pauli errors of weights one through three are either detected or lie in the stabilizer span.

finding.add · pending

Completed the exact bounded search over primes in 10428201..10428400 and produced the required artifact; no witness with multiplicity at least 16 was found, and the best multiplicity in-range was 10 at p=10428241, residue=3789711.

finding.add · signed event

Retire the unsupported prelaunch active-policy byte pair after preserving its content roots and confirming it admitted no state.

governance.policy_legacy_retirement · signed event

The exact remaining Erdős 730 gate is the exhaustive common-multiplicity event cover (23), followed by an explicit delta > 0 proving uniformly for X >= 2^57 that FirstPowerFar(X)/X + ShortTop(X)/X <= 1779/2500 - delta; neither step is proved at the pinned commit.

finding.add · pending

At first power, subtracting the fixed block shift leaves a multiple of the square prime modulus.

finding.add · pending

ExplicitDicksonAP12PrimeTupleSupplyK2 is the still-open assertion that for every U there is u >= U for which 48(12u)+29, 76(12u)+65, 38(12u)+23, and 48(12u)+41 are all prime; even this supplies only k=2, so the other fixed k >= 2 cases remain.

finding.add · pending

theorem erdosK2_of_explicitDicksonAP12PrimeTupleSupply (hSupply : ExplicitDicksonAP12PrimeTupleSupplyK2) : erdosFixed 2

finding.add · pending

The exact C2 residual is a universal no-surviving reduced-divisor split theorem; beyond that internal kernel, T4, full T6 and T7, the global kernel, and all later rungs remain unclaimed.

finding.add · pending

Coprime-refined existence-level C2 bridge. The extra coprimality condition is automatic from the split product identity, but recording it here matches the exact reduced-divisor obstruction used in the C2 analysis.

finding.add · pending

The remaining mathematical content for the pinned Erdős 686 refutation is exactly OddThueTail1000Hypothesis and LargeKSmoothHypothesis; equivalently, it is FinalResidual686Hypothesis.

finding.add · pending

The explicit final residual interface is logically equivalent to the conjunction of the updated odd-tail and large-smoothness hypotheses.

finding.add · pending

Conditional reduction of the r=5 case: if every balanced coloring of K_26 has extension demand exceeding 25 at some vertex, the Erdos-Gyarfas conjecture holds for r=5.

finding.add · pending

For Sidon sets A with |A| ~ N^{1/2}, the sumset A+A is equidistributed over residue classes mod m: each class holds ~1/m of A+A.

finding.add · pending

After the d = 2s - 2 closure, the one-stub all-nonbridge RL residual has 5 <= s and d <= 2s - 3; the multi-stub pair inequality and the final connected or 2-connected core remain separate obligations.

finding.add · pending

At d equal to twice the slack minus two, fully nonbridge corridor geometry, the rooted cut condition, injective simple demand pairs, legality, and same-color endpoints imply the exact RL internal-cost budget across all five canonical two-defect shapes.

finding.add · pending

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Lean kernel proof (prover-in-the-loop)

verifier.attach · legacy materialized

Erdős #18: 6 is a practical number (Erdos18.practicalH_six). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — via le_antisymm. Produced by the vela prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

Erdős #1054: f(5) = 0 (Erdos1054.f_undefined_at_3). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx. Produced by the vela prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

Erdős #17: 97 is the least non-cluster-prime (Erdos17.isClusterPrime_97_isLeast_non_cluster). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — via a decidable reformulation (cluster_iff) + interval_cases. Produced by the prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

Erdős #1052: every unitary perfect number is even (Erdos1052.even_of_isUnitaryPerfect). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — reconstructed ~168 lines. Produced by the vela prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

Erdős #1052 corollary: no unitary perfect number is odd (Erdos1052.not_odd_of_isUnitaryPerfect). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — whose proof INVOKES the accepted lemma even_of_isUnitaryPerfect (vf_6ccc854a9ab51bbb). A real lemma-inheritance event: an accepted verified lemma composed into a new verified theorem (Compounding B).

finding.add · legacy materialized

Erdős #138: W(1) = 1 (Erdos138.monoAPNumber_two_one). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — via sInf le_antisymm. Produced by the prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

Erdős #12: the good example (Erdos12.isGood_example). Kernel-clean Lean proof — axioms {propext, Classical.choice, Quot.sound}, no sorryAx — ported AlphaProof reference. Produced by the vela prover-in-the-loop foundry; verified by the Lean kernel.

finding.add · legacy materialized

The Lean 4 theorem `Erdos1052.isUnitaryPerfect_146361946186458562560000` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): 146361946186458562560000 is a unitary perfect number (the sum of its unitary divisors is twice itself). Closes a previously-`sorry` decl in google-deepmind/formal-conjectures Erdős Problem 1052.

finding.add · legacy materialized

OEIS A309370 a(5) >= 6: a Sidon set of 6 distinct binary 5-vectors with all pairwise sums distinct.

finding.add · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

backfill frozen verifier re-check

verifier.attach · pending

OEIS A309370 a(6) >= 15: a Sidon set of 15 distinct binary vectors in {0,1}^6 under componentwise integer addition, all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · pending

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

finding.retract · legacy materialized

Erdős #475 (distinct partial sums), finite confirmation: for every prime p ∈ {2,3,5,7,11,13}, all nonempty A ⊆ F_p\{0} admit an ordering with distinct partial sums mod p (subset counts 1,3,15,63,1023,4095 checked exhaustively). The question over all primes is the open problem.

finding.add · legacy materialized

Erdős #366, finite confirmation: no 2-full n with n+1 3-full in [1, 10000000]. The question over all integers is the open problem.

finding.add · legacy materialized

Erdős #364, finite confirmation: no three consecutive powerful integers in [1, 1000000] (consecutive powerful pairs do occur, e.g. 8,9). The question over all integers is the open problem.

finding.add · legacy materialized

Erdős #306, finite confirmation: 64 reduced a/b (b squarefree) each expand as distinct squarefree-semiprime Egyptian unit fractions. The question over all positive rationals is the open problem.

finding.add · legacy materialized

Erdős–Straus (#242, distinct variant), finite confirmation: for all 3 ≤ n ≤ 10000, 4/n = 1/x+1/y+1/z has an exact decomposition with x < y < z (9998 cases). The uniform proof over all n is the open problem.

finding.add · legacy materialized

Erdős #398 (Brocard), finite confirmation: for all 1 ≤ n ≤ 2000, n!+1 is a perfect square exactly for n ∈ {4,5,7}; every other n carries a quadratic-non-residue certificate. The conjecture over all n remains open.

finding.add · legacy materialized

a Costas array of order 7. Frozen-verified by vela-verify (costas kind).

finding.add · legacy materialized

OEIS A347025 a(6) >= 22: a union-free family of 22 subsets of {1..6} (no member is the union of others). Frozen-verified by vela-verify (union_free kind).

finding.add · legacy materialized

OEIS A394031 a(7) >= 12: a Sidon set of 12 elements in GF(2)^7 (all pairwise XORs distinct). Frozen-verified by vela-verify (gf2_sidon kind).

finding.add · legacy materialized

OEIS A321531 a(7) >= 11: a placement of 7 non-attacking rooks with 11 distinct direction classes. Frozen-verified by vela-verify (rook_directions kind).

finding.add · legacy materialized

OEIS A321531 a(8) >= 14: a placement of 8 non-attacking rooks with 14 distinct direction classes. Frozen-verified by vela-verify (rook_directions kind).

finding.add · legacy materialized

OEIS A394031 a(6) >= 9: a Sidon set of 9 elements in GF(2)^6 (all pairwise XORs distinct). Frozen-verified by vela-verify (gf2_sidon kind).

finding.add · legacy materialized

Erdős 650, axis-3 divergence: the hosted Lean proof does not certify the informal lower-bound argument it formalizes. The informal proof (GPT 5.4 Pro, prompted by He, Li, and Tang) contained a gap; Aristotle's formalization repaired it in-flight, and the gap surfaced only in the authors' arXiv write-up. Recorded per sources/informal_notes.yaml; source https://www.erdosproblems.com/forum/thread/650

finding.add · legacy materialized

FC statement draft for Erdős #426: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #512: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #209: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #328: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #639: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #353: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #206: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #621: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #403: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #464: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #648: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #71: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 199 (FormalConjectures/ErdosProblems/199.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 296 (FormalConjectures/ErdosProblems/296.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 904 (FormalConjectures/ErdosProblems/904.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 519 (FormalConjectures/ErdosProblems/519.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 453 (FormalConjectures/ErdosProblems/453.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 134 (FormalConjectures/ErdosProblems/134.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 476 (FormalConjectures/ErdosProblems/476.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 224 (FormalConjectures/ErdosProblems/224.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 493 (FormalConjectures/ErdosProblems/493.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 246 (FormalConjectures/ErdosProblems/246.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 1125 (FormalConjectures/ErdosProblems/1125.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 540 (FormalConjectures/ErdosProblems/540.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 419 (FormalConjectures/ErdosProblems/419.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 34 (FormalConjectures/ErdosProblems/34.lean, PR #4345) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 226 (FormalConjectures/ErdosProblems/226.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 178 (FormalConjectures/ErdosProblems/178.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 729 (FormalConjectures/ErdosProblems/729.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 281 (FormalConjectures/ErdosProblems/281.lean, PR #4346) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 47 (FormalConjectures/ErdosProblems/47.lean, PR #4345) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 1090 (FormalConjectures/ErdosProblems/1090.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 923 (FormalConjectures/ErdosProblems/923.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 31 (FormalConjectures/ErdosProblems/31.lean, PR #4345) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 871 (FormalConjectures/ErdosProblems/871.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 363 (FormalConjectures/ErdosProblems/363.lean, merged #4343) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 1126 (FormalConjectures/ErdosProblems/1126.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 532 (FormalConjectures/ErdosProblems/532.lean, merged #4319) faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 280 (FormalConjectures/ErdosProblems/280.lean, PR #4345) faithfully represents the informal problem.

finding.add · legacy materialized

FC statement draft for Erdős #646: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #537: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #502: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #484: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #497: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #618: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #443: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #582: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #487: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

FC statement draft for Erdős #498: gate green (lake build + extract_names + link rule)

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 429 (statements/429/429.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 401 (statements/401/401.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 164 (statements/164/164.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 333 (statements/333/333.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 369 (statements/369/369.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 93 (statements/93/93.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 314 (statements/314/314.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 24 (statements/24/24.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 315 (statements/315/315.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The drafted Formal Conjectures statement for Erdős problem 435 (statements/435/435.lean) faithfully represents the boxed problem; machine verdict on the linked hosted proof: unconditional (plby).

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 435 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 429 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 401 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 369 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 333 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 315 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 314 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 164 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 93 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement drafted for Erdős problem 24 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 258 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 1148 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 205 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 337 faithfully represents the informal problem.

finding.add · legacy materialized

The Formal Conjectures statement for Erdős problem 214 faithfully represents the informal problem.

finding.add · legacy materialized

Duplicate of canonical vf_bf7707a82c7bb252 (same claim OEIS A309370 a(10)>=66); its only backing artifact was the retired legacy remote-mode record va_86d1eafa7a5efdd5. The canonical finding is frozen-verifier-backed by sidon-a10.witness.json.

finding.retract · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

backfill frozen verifier re-check

verifier.attach · legacy materialized

OEIS A309370 a(24) >= 7179: a Sidon set of 7179 distinct binary vectors in {0,1}^24 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(18) >= 1010: a Sidon set of 1010 distinct binary vectors in {0,1}^18 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(7) >= 24: a Sidon set of 24 distinct binary vectors in {0,1}^7 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(8) >= 33: a Sidon set of 33 distinct binary vectors in {0,1}^8 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(15) >= 364: a Sidon set of 364 distinct binary vectors in {0,1}^15 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(16) >= 505: a Sidon set of 505 distinct binary vectors in {0,1}^16 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(9) >= 47: a Sidon set of 47 distinct binary vectors in {0,1}^9 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(10) >= 66: a Sidon set of 66 distinct binary vectors in {0,1}^10 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(22) >= 3770: a Sidon set of 3770 distinct binary vectors in {0,1}^22 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(14) >= 257: a Sidon set of 257 distinct binary vectors in {0,1}^14 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(12) >= 133: a Sidon set of 133 distinct binary vectors in {0,1}^12 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(11) >= 92: a Sidon set of 92 distinct binary vectors in {0,1}^11 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(17) >= 712: a Sidon set of 712 distinct binary vectors in {0,1}^17 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(19) >= 1435: a Sidon set of 1435 distinct binary vectors in {0,1}^19 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(21) >= 2694: a Sidon set of 2694 distinct binary vectors in {0,1}^21 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(13) >= 185: a Sidon set of 185 distinct binary vectors in {0,1}^13 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(23) >= 5179: a Sidon set of 5179 distinct binary vectors in {0,1}^23 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

OEIS A309370 a(20) >= 1989: a Sidon set of 1989 distinct binary vectors in {0,1}^20 under componentwise integer addition, with all pairwise sums distinct. Frozen-verified by vela-verify (sidon kind).

finding.add · legacy materialized

The Lean 4 theorem `Erdos257.erdos_257.variants.tsum_top_eq` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): the Lambert-series identity ∑_{n≥1} 1/(2^n - 1) = ∑_{n≥1} d(n)/2^n, where d(n) is the number of divisors of n. Closes a previously-open, UNCLAIMED `sorry` (category: textbook) in google-deepmind/formal-conjectures Erdős Problem 257.

finding.add · legacy materialized

Import artifact va_e76262c0020bf91d from artifact packet cap_beef856ac1c8e4ce

artifact.assert · legacy materialized

Import artifact va_742c51b3b65b701b from artifact packet cap_7a0d0ee2195e3fec

artifact.assert · signed event

Import artifact va_5af1bc8466dbfe23 from artifact packet cap_f41de5f08328c24e

artifact.assert · signed event

Import artifact va_115101bafeb9da86 from artifact packet cap_34c4f0e25c5b7011

artifact.assert · signed event

Automated reproduction of 'Re-verify the B_3 complete-frontier certificates (OEIS A396704): every recorded B_3 set in {0,1}^n is a valid B_3 set of the stated size, a frozen-verifier check of the maximum-size sequence 1, 2, 3, 4, 6, 8, 11.' succeeded (exit code 0).

finding.add · signed event

Import artifact repro_output_vtask_6db2a995822dfb91 from artifact packet cap_repro_vtask_6db2a995822dfb91

artifact.assert · signed event

The Lean 4 theorem `Erdos828.erdos_828.variants.phi_dvd_self_iff_pow2_pow3` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): for n : ℕ, Euler's totient φ(n) divides n if and only if n ≤ 1 or n = 2^a · 3^b for some a > 0 and b ≥ 0. Closes a previously-open `sorry` (category: textbook) in google-deepmind/formal-conjectures Erdős Problem 828.

finding.add · legacy materialized

The Lean 4 theorem `Erdos829.sumRep_cubes_three` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): the number of ordered representations of 3 as a sum of two perfect cubes is 0, i.e. 3 is not the sum of two cubes. Closes a previously-open `sorry` (category: test) in google-deepmind/formal-conjectures Erdős Problem 829.

finding.add · legacy materialized

The Lean 4 theorem `erdos_1150.variants.parseval_lower_bound` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): for every polynomial P over ℂ of degree n whose coefficients (indices 0..n) all lie in {-1, 1}, the supremum of |P(z)| over the unit circle |z| = 1 is at least √(n+1). This closes a previously-open `sorry` (category: textbook) attached to Erdős Problem 1150 in google-deepmind/formal-conjectures.

finding.add · legacy materialized

OEIS A309370 a(10) >= 66: a verified Sidon set of 66 distinct binary vectors in {0,1}^10 (componentwise integer addition into {0,1,2}^10; all 2211 pairwise sums a+b (a<=b) distinct), improving the live OEIS public lower bound a(10) >= 63 by +3 and the prior local best 65 by +1. Found by an Opus-4.8 Canopus-loop proposer (no-context arm, local search); re-verified from scratch by verify_construction.verify_sidon (frozen gate). Witness sha256:6a358e229f98b723…

finding.add · legacy materialized

The Lean 4 theorem `Erdos1054.f_undefined_at_2` — f 2 = 0 — for the Erdős-1054 function f(n) = least m such that n is a sum of the k smallest divisors of m (some k ≥ 1), f is UNDEFINED at n=2 (junk value 0). Proof: any such sum is 1 + R where the i=0 term is the least divisor 1 and every other term is 0 or a strictly larger divisor (≥ 2), so the sum is never 2. — is formally proven and kernel-verified in formal-conjectures (zero `sorry`, no extra axioms). Verifier: lean4-kernel + Mathlib v4.27.0 (lake build green; `#print axioms` = [propext, Classical.choice, Quot.sound] only — NO sorryAx).

finding.add · legacy materialized

Import artifact va_f78d5e0808a9ac34 from artifact packet cap_6fcdb44f3a2ff0c6

artifact.assert · legacy materialized

The Lean 4 theorem `Erdos961.erdos_961.variants.sylvester_schur_1_1` — Erdos961Prop 1 1 (the n=k=1 instance of Sylvester–Schur: every m ≥ 2 has, in {m}, an element that is not 2-smooth) — is formally proven and kernel-verified in formal-conjectures (zero `sorry`, no extra axioms). Verifier: lean4-kernel + Mathlib (lake build green; the declaration's proof term carries no `sorry` and no extra axioms).

finding.add · legacy materialized

Import artifact va_370c3b127f446b92 from artifact packet cap_4af431152a035fa4

artifact.assert · legacy materialized

The largest distance of a single-logical-qubit stabilizer code at length 10, [[10,1,d]], is open within the band d in [3,4]; whether a [[10,1,4]] stabilizer code exists is undetermined here.

finding.add · legacy materialized

The Shor code [[9,1,3]] (concatenated bit- and phase-flip repetition) encodes 1 logical qubit in 9 physical qubits with distance 3, verified from its eight stabilizer generators.

finding.add · legacy materialized

The Steane code [[7,1,3]] (CSS from the [7,4,3] Hamming code) encodes 1 logical qubit in 7 physical qubits with distance 3, verified from its six stabilizer generators.

finding.add · legacy materialized

The perfect five-qubit code [[5,1,3]] (cyclic stabilizers XZZXI and rotations) encodes 1 logical qubit in 5 physical qubits with distance 3, and is optimal at its length.

finding.add · legacy materialized

The [[4,2,2]] code with stabilizers XXXX, ZZZZ encodes 2 logical qubits in 4 physical qubits with distance 2, verified by exact recomputation of k and d.

finding.add · legacy materialized

Import artifact va_qcverify00000001 from artifact packet cap_a1b2c3d4e5f60718

artifact.assert · legacy materialized

Attach source-backed abstract span for the Ellenberg-Gijswijt cap-set result; leaves the numeric constant as methodology context rather than new accepted evidence.

finding.span_repair · legacy materialized

Exact arXiv locator for Ellenberg-Gijswijt cap-set result; records a reviewable source locator without changing the finding assertion.

evidence_atom.locator_repair · legacy materialized

Attach source-backed abstract span for the Bloom-Sisask Roth log-barrier result; does not change the assertion.

finding.span_repair · legacy materialized

Exact arXiv locator for Bloom-Sisask Roth log-barrier result; records a reviewable source locator without changing the finding assertion.

evidence_atom.locator_repair · legacy materialized

Attach source-backed abstract span for the Croot-Lev-Pach Z_4^n bound; does not change the assertion.

finding.span_repair · legacy materialized

Exact arXiv locator for Croot-Lev-Pach progression-free Z_4^n result; records a reviewable source locator without changing the finding assertion.

evidence_atom.locator_repair · legacy materialized

Cilleruelo 2010: B_2[g] sets in {1,...,N} (sets where each integer has at most g representations as a sum of two elements) have cardinality at most sqrt(g*N) + O(N^(1/4)), generalizing the Lindstrom-Erdos-Turan bound from g=1 to g>=2.

finding.add · signed event

Ruzsa triangle inequality: for any finite subsets X, Y, Z of an abelian group, |X-Z| * |Y| <= |X-Y| * |Z-Y|. A foundational sumset inequality underpinning Plunnecke-Ruzsa and the Freiman-Ruzsa theorem.

finding.add · signed event

Bose-Chowla 1962 construction: for any prime power q, the set of integers x in {0,...,q^2-2} satisfying alpha^x = alpha + x mod (alpha-generated finite field) yields a Sidon set of size q in {1,...,q^2}, attaining the asymptotic upper bound of sqrt(N).

finding.add · signed event

The primes contain arbitrarily long arithmetic progressions: for every k there is a k-term arithmetic progression of primes.

finding.add · signed event

Tao 2007 higher-order Fourier analysis program: Gowers U^s norms admit an inverse theorem characterizing functions with non-negligible U^s norm as correlating with degree-s nilsequences. The U^3 case is the load-bearing first step beyond classical Fourier analysis.

finding.add · signed event

Croot-Lev-Pach: progression-free subsets of (Z/4Z)^n have cardinality at most c * 4^(0.926n) via the polynomial method, dramatically improving Behrend-style bounds for cap sets.

finding.add · signed event

Erdos-Ko 1957: explicit Sidon set construction in {1,...,N} of size sqrt(N) - O(N^(1/4)), matching the Erdos-Turan upper bound asymptotically and establishing Theta(sqrt(N)) as the correct order of magnitude.

finding.add · signed event

Schoen-Shkredov: density alpha > exp(-c * (log N)^{1/4}) suffices for 3-APs via combined Fourier and Bohr-set decomposition methods.

finding.add · legacy materialized

Ellenberg-Gijswijt extend Croot-Lev-Pach to prove a 3-AP-free subset of F_3^n has size at most 2.756^n, settling the cap-set problem up to a constant in the exponent.

finding.add · legacy materialized

The polynomial method bounds 3-AP-free subsets of (Z/4Z)^n by 4^{0.926n}, far below the 4^n total, breaking the previous logarithmic-style bounds for cap-set-style problems.

finding.add · legacy materialized

A Bohr neighborhood B(Lambda, rho) is the set of x in Z/NZ where |gamma * x / N| < rho for all gamma in Lambda; its dimension d = |Lambda| controls density |B| / N >= rho^d, enabling Fourier-analytic density-increment iterations.

finding.add · legacy materialized

Freiman's theorem: a finite set A of integers with |A+A| <= K|A| is contained in a generalized arithmetic progression of dimension at most d(K) and size at most f(K) * |A|.

finding.add · legacy materialized

Ruzsa covering lemma: if |A+B| <= K|A|, then B is contained in the sumset A - A translated by at most K elements; the engine of small-doubling structure theorems.

finding.add · legacy materialized

Plunnecke-Ruzsa inequality: if |A+A| <= K|A|, then |kA - lA| <= K^{k+l} * |A| for all nonnegative integers k, l.

finding.add · legacy materialized

Functions with large Gowers U^{s+1}-norm correlate with nilsequences of step s; this inverse theorem is the analytic engine behind quantitative Szemeredi for arbitrary k.

finding.add · legacy materialized

Gowers gave the first quantitative proof of Szemeredi's theorem with effective bounds, introducing higher-order Fourier analysis (Gowers norms U^k) as the central tool.

finding.add · legacy materialized

Szemeredi's theorem: any subset of the natural numbers with positive upper density contains arbitrarily long arithmetic progressions.

finding.add · legacy materialized

Bloom-Sisask break the 'log barrier' for Roth: density alpha > 1 / (log N)^{1+c} for an absolute c > 0 suffices for a 3-AP, the first sub-1/log N bound.

finding.add · legacy materialized

Sanders' bound: density alpha > C * (log log N)^4 / log N is sufficient to guarantee a 3-term AP in any subset of {1,...,N}.

finding.add · legacy materialized

Bourgain's Fourier-analytic increment argument lowers the density threshold for 3-AP existence in {1,...,N} to alpha > C * (log log N)^2 / sqrt(log N).

finding.add · legacy materialized

Roth's theorem: any subset of {1,...,N} of density alpha > C / log log N contains a nontrivial 3-term arithmetic progression.

finding.add · legacy materialized

Behrend's construction yields subsets of {1,...,N} of size N * exp(-c * sqrt(log N)) containing no nontrivial 3-term arithmetic progression, the densest such known until 2020.

finding.add · legacy materialized

B_h sets, the h-fold generalization of Sidon sets, have maximum density satisfying |A| <= (h! * N)^{1/h} + O(N^{1/(2h)}) in {1,...,N}.

finding.add · legacy materialized

Lindstrom's upper bound for Sidon-set size in {1,...,N} is sqrt(N) + N^{1/4} + 1, tightening the Erdos-Turan bound by a factor of sqrt(2).

finding.add · legacy materialized

Singer's perfect-difference-set construction in projective planes yields Sidon sets in {1,...,N} of size sqrt(N) + O(N^{1/4}), matching the elementary upper bound up to lower-order terms.

finding.add · legacy materialized

Bound and construction look correct under the Nathanson hypothesis but I want a Lean stub before promoting to accepted-core. The proof step that reduces geometric to polynomial diameter needs an explicit witness.

finding.review · legacy materialized

The h-squared-dissociated set construction needed for the polynomial bound has diameter polynomial in k, replacing geometric components in the original construction.

finding.add · legacy materialized

For h>=3 the analog of N(h,k) admits a polynomial in k upper bound via h-squared-dissociated sets, replacing the prior exponential construction.

finding.add · legacy materialized

A Sidon set in {1,...,N} of size O(sqrt(N)) exists, attaining the elementary upper bound for h=2 sumsets up to a multiplicative constant.

finding.add · legacy materialized