AI Proof WatchKeep up with AI contributions

The exact solution of Bellman's lost-in-a-forest problem for the golden gnomon

Alexander Temerev, Alessio Doria

Temerev and Doria report that the minimum escape-path length for the golden gnomon, an isosceles triangle with unit equal sides and 36-degree base angles, is 1.282676025459… . A symmetric seven-piece path attains the value, and their lower bound covers every rectifiable competitor.

Sources for this record

What was already known

Exact optima were known for the equilateral triangle and base angles from 45 to 60 degrees. Gibbs had numerically predicted a seven-piece path near 36 degrees but had not proved its exact global optimum.

AI involvement AI-centered

The title disclosure credits Claude Fable 5, GPT 5.6 Sol and Claude Opus 5 with searching for the extremal path, drafting arguments and writing the Lean development. Temerev and Doria are the human authors; the source does not divide every proof idea by origin.

Models searched for the exact retained path and drafted arguments, while human authorship and unspecified mathematical direction prevent a stronger independence finding.

Importance Notable

The claimed proof gives the first exact optimum below the previously solved 45-degree range and an equivalent sharp worm-cover result for this triangle.

Limitations

Lean checks selected exact calibration, geometry and discrete certificates; compactness, hull surgery, planar incidence and parts of minimizer rigidity remain in prose. The full global optimum has no documented complete check.

Technical verification Partial

The paper reports Lean 4 checks of exact calibration and geometry certificates, rational inequalities and reusable discrete identities. Its Appendix B.3 explicitly leaves compactness, hull surgery, planar incidence and parts of minimizer rigidity in prose; the full global optimum is not machine-certified, and no complete human check is documented.

Formal checking

Exact rational interval certificate checking and formal proof of selected identities

Checker
Lean 4 kernel in the authors' reported development
Scope
Calibration root and scalar bounds, seven-piece geometry and support-window certificates, plus listed finite escape and ledger identities for the golden gnomon
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The exposition describes the mechanism, but the authors say models drafted arguments throughout and do not identify a person's own explanation of the central calibration and rigidity reasoning. Few is the evidence default, not a claim that the authors understand little.

Correction and publication history