finding record / formal-conjectures
recordedvf_f745c7b4d5f2efba
vf_f745c7b4d5f2efba
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.
Notation is rendered from the stored source. The pinned checkout remains the exact record.
- model_output
- theoretical
- 0 spans
- recorded
Record vrc_9bbf9c71470e3d36 (signed; recorded against the current head). Caveats: Kernel-verified locally (Lean v4.27.0, mathlib a3a10db0); the upstream formal-conjectures PR is the external acceptance step and requires the maintainer's action. | Establishes ONE unitary-perfect witness value, NOT the open Erdős 1052 question (the existence/classification of odd or further unitary perfect numbers) itself. | Proof ported from Sanexxxx777's formal-conjectures fork; author-of-record attribution is to the original proof author, not the foundry agent.. Artifacts: 1 hash-verified at propose.
- record:vrc_9bbf9c71470e3d36
- model_output
- Jul 6, 2026, 7:42 PM
- not recorded
- 0
Exact record identityFinding ID, frontier identity, and pinned Git source
- vf_f745c7b4d5f2efba
- 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