frontiers / frontier
Formal-conjectures Lean proofs (kernel-verified)
- id
- vfr_97d7d25957384f80
- license
- CC-BY-4.0
- findings
- 2
- accepted core
- 0
- contested
- 0
- links
- 0
- sources
- 2
- evidence
- 2
- avg conf
- 0.99
e4/4 · finding.asserted · reviewer:will · 2026-06-03 · null→5d1d
No statement authored. accepted findings
use this record
vela registry pull vfr_97d7d25957384f80vela reproduce projects/formal-conjectures-leanpast week quiet · last event 11d
recorded · 2 events
press the seal to re-verify on this device
Signals
Finding types
2 findings- theoretical2
Review state
2 findings- unreviewed2
Flow
Top findings
all stateThe 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).
0.99vf_b8e3badb634a19a0assertedwill· 11dThe 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).
0.99vf_bc277af6cc7a3216assertedwill· 11dShowing 2 of 2