What was already known
A 2017 question noted the planar lower bound √6 and the elementary volume upper bound 3. Stronger bounds for particular dimensions or asymptotic regimes had not supplied the cited explicit uniform proof.
AI involvement
Sébastien Palcoux posed the question and prompted the work. The project credits GPT-5.6 Pro with the mathematical argument, manuscript and substantive Lean proof.
The source credits the mathematical proof itself to GPT-5.6 Pro under Palcoux’s prompts.
- Supporting source (github.com) — Statements; proof map and dimension cases
Importance
Answers the exact no-prefactor universal-base question with a direct proof and formal certificate.
Limitations
The result does not give the best asymptotic exponent as n grows. The Lean development formalizes a volume-packing proof; a shorter spherical-cap argument in the manuscript is outside that check. No human mathematical check is documented.
Technical verification
The source reports a complete Lean 4/Mathlib proof, an axiom audit, and Comparator/NanoDa replay for the eight assessed claims.
Formal checking
Repository reports Lean proof, all-project axiom audit and independent kernel replay of selected statements.
- Checker
- Lean 4 and NanoDa kernels
- Scope
- Uniform bound, τ₂=6 and least-base statements in Solution.lean
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
A named human account of the volume-packing proof is not documented; this is an evidence-gap default.
Correction and publication history
The reported Lean result proves the optimal universal base √6 without a prefactor.
Read this published revision