Conjectures.io

Geometry

Green41.green_41.variants.polynomial_bound

Is ε−C\varepsilon^{-C} rotations enough?

References

  • [Ma15] Manners, Freddie. "A solution to the pyjama problem." Inventiones mathematicae 202.1 (2015): 239-270.
  • [KrLe25] Kravitz, Noah, and James Leng. "Quantitative pyjama." arXiv preprint arXiv:2510.17744 (2025).

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ C, ∃ ε₀ > 0, ∀ ε ∈ Set.Ioc 0 ε₀, ↑(Green41.minCopies ε) ≤ ε ^ (-C)

What you must prove

import FormalConjectures.GreensOpenProblems.«41»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green41.green_41.variants.polynomial_bound" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/41.lean

Source type SHA-256
sha256:f6ca32f1ba2650373ef5c0ae19a2eb5284e4ff67422cdd54a0fc2d24d4f05d00
Task id
fc-379fc029-variants-polynomial-bound-e319dd4b52-formalized-v1
Task commitment
sha256:b03e29d455ca0cdfd04536ac0969b2bf6243504ce1c04bffaccf487ef31d43be

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.