ten-proofs: assess additional contribution candidates

Updated against FC [`2a0126f6`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c) on 11 September 2026.

Erdős 146, 180 and 183 are already represented and link the pinned `openai/ten-proofs` results added by merged #4715. Do not add them again.

The remaining topics from the original proposal are contribution candidates, not an automatic import list:

| Topic | Original proof-repository file |
| --- | --- |
| Connes rigidity counterexample | `ConnesRigidity.lean` |
| Ehrhart volume bound | `EhrhartVolumeInequality.lean` |
| Non-sofic group | `NonSoficGroup.lean` |
| Sphere packing | `SpherePacking.lean` |
| Binary/spherical code bounds | `MetricCodes.lean` |
| Permanent formula lower bound | `Permanent.lean` |
| Quantum parallel repetition | `QuantumParallelRepetition.lean` |
| Closest vector problem hardness | `GapCVP.lean` |

A current source/name/reference search found explicit `ten-proofs` links only for the three Erdős problems. Green 42 already discusses the Cohn–Elkies scheme, so sphere-packing work needs a precise comparison with that existing statement. This search does not establish that no equivalent statement exists under another name.

Before taking a topic:

1. Check existing statements and open contributions for the exact claim.
2. Read an appropriate source and establish what the Lean statement should say.
3. Identify definitions and Mathlib prerequisites from the current libraries.
4. Confirm contributor interest and maintainer scope before proposing a focused contribution.

The old blanket claims about missing Mathlib APIs and proof-axiom cleanliness were not requalified here. A generated workspace or a proof link does not replace source fidelity or maintainer acceptance. These mathematical contributions are separate from #4394's toolkit release.

Original source: [openai/ten-proofs](https://github.com/openai/ten-proofs). This issue remains open for contributor-led, individually assessed work.

Start by checking existing statements and open contributions for the eight candidate topics, including the listed source files such as ConnesRigidity.lean, EhrhartVolumeInequality.lean, and SpherePacking.lean. Read an appropriate source, identify the required definitions and Mathlib prerequisites, and confirm contributor interest and maintainer scope. Done means proposing a focused contribution with a precise Lean statement and source fidelity.

Written by the indexing model from the issue text.