What was already known
The logarithmic spiral was conjectured optimal by Baeza-Yates, Culberson and Rawlins. Previous general lower bounds and stronger bounds under cyclic restrictions did not establish unrestricted optimality.
AI involvement
GPT-6 Astra, Claude Fable 5.1 and Claude Opus 5 helped find the reduction and storage function and write Lean modules and two interval-arithmetic verifiers. Humans directed the work and the manuscript documents audit-driven repairs.
Temerev credits GPT-6 Astra, Claude Fable 5.1 and Claude Opus 5 with finding the reduction and storage function, with human direction and audit-driven repairs.
Importance
Reports a matching unrestricted minimax bound for a longstanding geometric online-search problem.
Limitations
The reported Lean proofs cover specified reduction lemmas, and two Arb interval implementations check the certificate inequalities. Section 10 lists geometric and measure-theoretic steps outside the Lean formalization. The broader proof remains a source-reported result.
Technical verification
Section 10 reports Lean checks of selected lemmas and two Arb interval checks of the certificate. It expressly lists geometric and measure-theoretic steps not formalized, so the full theorem is not machine checked.
Formal checking
The author reports zero-sorry Lean checks of listed lemmas and two Arb interval certificate checks; Section 10 lists the unformalized steps.
- Checker
- Author-reported Lean 4 and Arb checkers
- Scope
- Selected polygonal, angular and bookkeeping lemmas plus the storage-function inequalities, not the full geometric reduction.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Temerev gives a detailed human-written outline and prose derivation of the reduction, control problem and storage-function certificate, documenting the central reasoning.
Correction and publication history
Primary-source review under the four independent curation dimensions. This restores the original archived contribution identity without subscriber notification.
Read this published revision