finding record / formal-conjectures
recordedvf_48d089ada508111d
vf_48d089ada508111d
Canonical assertion
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.
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:test; result:no_representation; open_sorry_closed:true
Provenance summary
- cap_f41de5f08328c24e · vc_3fe62fa30a5792b8
- model_output
- Jun 14, 2026, 12:00 AM
- not recorded
- 1
Exact record identityFinding ID, frontier identity, and pinned Git source
- vf_48d089ada508111d
- 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