ProofAtlas

Convex geometry · formal theorem

Polygonal Direct-Motion Worm Lower Bound

Four Lean-checked pointwise area inequalities cover finite polygonal worms and all unit worms, with direct motions or reflections allowed. Their strict rational corollaries give the lower bound 0.23743658226923856768; the exact optimum remains open.

Scope: Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.

Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Moser worm lower-bound statement mapFour exact Lean theorem pairs bound the area of each convex cover universal for finite polygonal worms or all unit worms, with direct motions or reflections allowed.
Exact scope: Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.

Exact formal proposition

Hypotheses and conclusion

theorem polygonalDirect_area_ge_THat (C : ConvexCover) (hC : PlacesEveryUnitPolyline C .direct) : THat ≤ coverArea C

Result boundary

What this theorem does—and does not—establish

Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 72 Lean files · 4 evidence records · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Technical evidence, source identity, and assumptions
Main Lean declaration
polygonalDirect_area_ge_THat
Source commit
c9254797b42c

Mechanical evidence

Lean verification

These fields support the exact Lean declaration, not a broader informal claim.

Why ProofAtlas acceptance is still pending: the supplied release audit records a successful one-worker rehash build, no unfinished proof commands, and the reported axiom closure. It does not retain the complete command/output transcript and clean-source collection record required for accepted-result status.

Artifact ID
artifact.moser-worm.polygonal-direct-area.lean-package.v001
Declarations covered by recorded evidence
MoserWorm.polygonalDirect_area_ge_THat
MoserWorm.polygonalDirect_area_gt_published
Lean build
passed
Recorded build time
Not retained in the supplied release audit
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.30.0-rc2
Recorded source commit
c9254797b42c2a89acb00281c0822c7d6fc21923
Source SHA-256
sha256:2f873beecb35c02bf40af8516eaef6393bb34533d9271e79eb8085b76c1e263f
Statement alignment
under review

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Independent review

Review open

Review remains open for the exact statement, scope, evidence, and public wording. See the remaining review questions.

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Paper author
Lech Mazur

Contributions

  • Direct contributionOpenAI Codex, OpenAI GPT-5.6 Pro

    OpenAI GPT-5.6 Pro and OpenAI Codex have source-reported roles in mathematical exploration, proof development, computational testing, adversarial auditing, formalization, and exposition.

    • Computation
    • Exposition
    • Formalization
    • Gap or error discovery
    • Proof strategy
  • Direct contributionLech Mazur

    Lech Mazur is the paper author and accountable editor and directed the AI-assisted research, verification process, output selection, and reconciliation.

    • Exposition
    • Proof strategy
    • Research direction

Citation

Cite this release

Use the version-specific citation so the authorship, scope, and public record remain attached.

Release history

Versions and public record

Release
Paper release
Version
public version of September 2, 2026
Published
Canonical page
Open canonical page
Earlier release
credit.release.moser-worm-mixed-area-lower-bound.v001

Release chronology

This version is part of the release history. No independent external timestamp is claimed.

Scope of this release

  • No accepted-result record exists for the Moser worm artifacts in this snapshot.
  • No independent external priority anchor, specialist review, or independent statement-alignment review is recorded.
  • The paper's infimum notation is not a Lean declaration in this release; the checked endpoints are stronger pointwise cover inequalities.
  • The paper, bundle, supplied infographic, and ProofAtlas covers are authorized for ProofAtlas distribution but have no general open-content license.
  • The result improves a lower bound and does not determine the optimal cover or solve Moser's convex worm problem.