Kernel-verified Lean theorems (prover-in-the-loop): review

Proposal standing and signed decisions at this exact published snapshot.

Authority boundary

Evidence is not acceptance

Verification can support a proposal. It cannot supply the scientific decision.

EvidenceA bounded artifact is recorded.
VerifierA named check reproduces the result.
ProposalA claim enters review without changing accepted state.
DecisionA registered human or exact policy supplies authority.
StandingOnly the signed decision changes accepted state.

28
all proposals: 1
pending: 24
applied: 3
rejected / withdrawn

Latest terminal decision

Jul 7, 2026, 2:51 PM

appliedvpr_fabcc7ac69bfd67d

kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed

Signed by reviewer:will-blair; provenance: legacy materialized.

Exact decision provenanceDecision event, plan, proposal, and Receipt roots

Decision event: not recorded
Decision plan: not recorded
Proposal: not recorded
Receipt: not recorded

Proposal ledger

standing, not verdict quality

28 proposals

vpr_f4380d0b90a35799
finding.add · Jul 19, 2026, 5:13 AM
pending review
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.
Inspect exact provenance
Proposal
sha256:c82bf606d4e8dc66c10fa41ebf72ba7558e4f51886ba2759910ffeb91521b015
Receipt
sha256:aeede68ff2bccec34a350e688abd036468bc63b471883fbbc7bf47e5366d2e6a
Decision plan
not recorded
Decision event
not recorded
vpr_fabcc7ac69bfd67d
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_c04d6fa4ccd1dbd3
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_854df7b19736a200
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_a4a18caaa415b4b3
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_495f488451d0512a
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_2c8b1990cefad049
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_8cc7b59a27ca9acb
verifier.attach · Jul 7, 2026, 2:51 PM
applied
Lean kernel proof (prover-in-the-loop)
kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_d24a500f42a2d2a4
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_934b7beadabb9968
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_8ec1cabc640b3756
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_8d8e568d7faf9a4e
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_80f670704bb33dc2
finding.add · Jul 6, 2026, 9:15 PM
applied
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).
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_5c6ae77ffa9a6251
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_3228eb63f2d4635d
finding.add · Jul 6, 2026, 9:15 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_f6ec5466eb74501b
finding.add · Jul 6, 2026, 8:27 PM
applied
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.
accepted via sign session
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_d908e3fdbc6248e1
finding.add · Jun 15, 2026, 4:33 PM
applied
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.
Erdős #257 tsum_top_eq: genuinely novel kernel-clean close; PR #4269 open upstream.
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_8661f354aa2ad568
artifact.assert · Jun 15, 2026, 4:33 PM
applied
Import artifact va_e76262c0020bf91d from artifact packet cap_beef856ac1c8e4ce
Erdős #257 tsum_top_eq: kernel-clean Lean 4 proof artifact (no sorryAx).
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_bcd2fa4d3b821a93
artifact.assert · Jun 15, 2026, 4:33 PM
rejected
Import artifact va_742c51b3b65b701b from artifact packet cap_7a0d0ee2195e3fec
Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
vev_96129c5e8f98d01f
vpr_99706386ddc82e18
artifact.assert · Jun 15, 2026, 4:33 PM
rejected
Import artifact va_5af1bc8466dbfe23 from artifact packet cap_f41de5f08328c24e
Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
vev_a9f3e843b0ca5739
vpr_3a048ea6d174f094
artifact.assert · Jun 15, 2026, 4:33 PM
rejected
Import artifact va_115101bafeb9da86 from artifact packet cap_34c4f0e25c5b7011
Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
vev_73551f8775cf2671
vpr_7edc56a44d11e310
finding.add · Jun 14, 2026, 9:59 PM
applied
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.
Kernel-verified Lean proof (no sorryAx): phi(n)|n iff n<=1 or n=2^a 3^b, a>0; closes the textbook sorry in Erdos 828
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_0b5674927668851b
finding.add · Jun 14, 2026, 9:50 PM
applied
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.
Kernel-verified Lean proof (no sorryAx): 3 is not a sum of two cubes; closes the test-category sorry in Erdos 829
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_e90483294cefbdd4
finding.add · Jun 14, 2026, 9:29 PM
applied
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.
Kernel-verified Lean proof (no sorryAx) of the Parseval sqrt(n+1) lower bound for ±1 polynomials; closes the open textbook sorry in Erdos 1150
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded
vpr_46734a4a9d2acfe0
finding.add · Jun 3, 2026, 9:03 PM
applied
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).
lake green, axiom-clean, newly-closed textbook sorry
Inspect exact provenance
Proposal
not recorded
Receipt
not recorded
Decision plan
not recorded
Decision event
not recorded

Proposal	Claim and exact roots	Standing	Recorded
vpr_f4380d0b90a35799 finding.add	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.Show roots Proposal sha256:c82bf606d4e8dc66c10fa41ebf72ba7558e4f51886ba2759910ffeb91521b015 Receipt sha256:aeede68ff2bccec34a350e688abd036468bc63b471883fbbc7bf47e5366d2e6a Decision plan not recorded Decision event not recorded	pending review	Jul 19, 2026, 5:13 AM
vpr_fabcc7ac69bfd67d verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_c04d6fa4ccd1dbd3 verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_854df7b19736a200 verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_a4a18caaa415b4b3 verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_495f488451d0512a verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_2c8b1990cefad049 verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_8cc7b59a27ca9acb verifier.attach	Lean kernel proof (prover-in-the-loop)Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded kernel-verified witness (foundry lean-run, no sorryAx); re-homed theorem upgraded from claim to witnessed	applied	Jul 7, 2026, 2:51 PM
vpr_d24a500f42a2d2a4 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_934b7beadabb9968 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_8ec1cabc640b3756 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_8d8e568d7faf9a4e finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_80f670704bb33dc2 finding.add	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).Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_5c6ae77ffa9a6251 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_3228eb63f2d4635d finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 9:15 PM
vpr_f6ec5466eb74501b finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded accepted via sign session	applied	Jul 6, 2026, 8:27 PM
vpr_d908e3fdbc6248e1 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded Erdős #257 tsum_top_eq: genuinely novel kernel-clean close; PR #4269 open upstream.	applied	Jun 15, 2026, 4:33 PM
vpr_8661f354aa2ad568 artifact.assert	Import artifact va_e76262c0020bf91d from artifact packet cap_beef856ac1c8e4ceShow roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded Erdős #257 tsum_top_eq: kernel-clean Lean 4 proof artifact (no sorryAx).	applied	Jun 15, 2026, 4:33 PM
vpr_bcd2fa4d3b821a93 artifact.assert	Import artifact va_742c51b3b65b701b from artifact packet cap_7a0d0ee2195e3fecShow roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event vev_96129c5e8f98d01f Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.	rejected	Jun 15, 2026, 4:33 PM
vpr_99706386ddc82e18 artifact.assert	Import artifact va_5af1bc8466dbfe23 from artifact packet cap_f41de5f08328c24eShow roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event vev_a9f3e843b0ca5739 Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.	rejected	Jun 15, 2026, 4:33 PM
vpr_3a048ea6d174f094 artifact.assert	Import artifact va_115101bafeb9da86 from artifact packet cap_34c4f0e25c5b7011Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event vev_73551f8775cf2671 Bulk triage 2026-06-15: automated draft (watcher/extractor/ingest), not adjudicated; declining to keep the review gate meaningful. Recoverable from its Carina packet if needed.	rejected	Jun 15, 2026, 4:33 PM
vpr_7edc56a44d11e310 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded Kernel-verified Lean proof (no sorryAx): phi(n)\|n iff n<=1 or n=2^a 3^b, a>0; closes the textbook sorry in Erdos 828	applied	Jun 14, 2026, 9:59 PM
vpr_0b5674927668851b finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded Kernel-verified Lean proof (no sorryAx): 3 is not a sum of two cubes; closes the test-category sorry in Erdos 829	applied	Jun 14, 2026, 9:50 PM
vpr_e90483294cefbdd4 finding.add	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.Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded Kernel-verified Lean proof (no sorryAx) of the Parseval sqrt(n+1) lower bound for ±1 polynomials; closes the open textbook sorry in Erdos 1150	applied	Jun 14, 2026, 9:29 PM
vpr_46734a4a9d2acfe0 finding.add	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).Show roots Proposal not recorded Receipt not recorded Decision plan not recorded Decision event not recorded lake green, axiom-clean, newly-closed textbook sorry	applied	Jun 3, 2026, 9:03 PM

Page 1 of 2