finding record / formal-conjectures
recordedvf_99c872a66cc24fb6
vf_99c872a66cc24fb6
Canonical assertion
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.
Notation is rendered from the stored source. The pinned checkout remains the exact record.
- model_output
- theoretical
- 1 spans
- recorded
Scope and conditions
theoretical
domain:number_theory; verifier:lean4_kernel; category:textbook; result:totient_divides_characterization; open_sorry_closed:true
Provenance summary
- cap_7a0d0ee2195e3fec · vc_656866803ec4c903
- model_output
- Jun 14, 2026, 12:00 AM
- not recorded
- 1
Exact record identityFinding ID, frontier identity, and pinned Git source
- vf_99c872a66cc24fb6
- vfr_97d7d25957384f80
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- a24f2c67b52a5b3c9163438243b95351bbc8e296
Exact source and rootsGit 2705e4db4ffb and content-addressed ledgers
Source identity
- Commit
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- Tree
- a24f2c67b52a5b3c9163438243b95351bbc8e296
- Committed
- 2026-07-19T05:13:20Z
- Repository
- Open source
Content roots
- Event log
- sha256:c4a00883ab7468dcce59c368b81fd09e45366b21af8e34979d7a639d73a8d32c
- Snapshot
- sha256:45fa712bd6d9a8d4c8514a7cba107e7f814f2c1368805abd577e762ccb6123a4
- Proposals
- sha256:ba47ddf5c16ed567ddf835385066e3fc294b447bc0eabd3f9820f5e707efb39e
- Actor registry
- sha256:f52d59b1db885f467c66a29335ada68544a09da5f3869723461100eed0aac79e
- Artifacts
- sha256:fbd7e05b185cd06bc06484e8b0216c17c5263a71d8481ca38e574e9b2c5156d8