Import Kahn-Kalai expectation-threshold theorem

[Vilin97]

Summary

• imports Dan Clemens Posch's Apache-2.0 Lean formalization at upstream commit 641aa75
• exposes the audited headline declarations KahnKalai.covering_theorem (Tran–Vu Theorem 2.3, L = 1000) and KahnKalai.park_pham (Park–Pham / Kahn–Kalai, with witness K = 100000)
• registers the project and updates the aggregate import; generated README/NOTICE changes are intentionally left to the repository's metadata workflow

Daily-import eligibility and selection

The discovery window was exactly [2026-08-25T13:01:04Z, 2026-09-01T13:01:04Z]. The selected completion commit was published at 2026-09-01T06:13:27Z, inside that interval. Searches covered GitHub, Reservoir, arXiv, public Zulip indexing, and public X indexing. No prior Lean Pool module, merged PR, open PR, or historical path matched this formalization.

Higher-profile fresh candidates QuadraticIterates and UlmsTheorem were already merged as #371 and #369. Other current candidates were rejected for one or more of: incomplete headline proof, explicit axioms in the advertised result, missing/unclear license, unsupported dependencies, very large cleanup burden, or substantially lower significance/reuse.

Fidelity and provenance

• the public theorem types are verbatim the upstream audited Challenge.lean surface
• the implementation closure is 2,787 lines across seven modules; no challenge scaffold, scripts, PDFs, or isolated scratch files are imported
• compared scope: Tran–Vu Theorems 2.3 and 1.1, finite-type ground sets, base-2 logarithm, L = 1000; not compared: the L ≈ 3.998 optimization, Bell's epsilon-covering theorem, or paper sections 3–4
• upstream records AI-assisted development with Grok 4.6, coordinated/formalized by Dan Clemens Posch, and no independent upstream reviewer; the registry records provenance: AI
• verified upstream Apache-2.0 license; local NOTICE regeneration produced the expected attribution, but the generated file is omitted by the content-only PR policy

Port and performance work

• updates the import namespace for Lean Pool and ports Lean 4.32/mathlib 4.32 code to Lean 4.34.0-rc1
• replaces broad imports with the precise transitive closure and removes all three global heartbeat overrides
• fixes all warnings, documents public definitions, and splits the two over-limit monolithic proofs into reusable intermediate lemmas
• dependency-warm clean build improved from 20.68 s / 3,609,572 KiB / 3,123 jobs to 16.09 s / 2,868,856 KiB / 2,216 jobs: wall time -22.2%, peak RSS -20.5%, build jobs -29.0%

Validation

• lake build LeanPool.KahnKalai
• lake build LeanPool (9,414 jobs)
• scripts/ci/build-challenges.sh (only the expected pre-existing challenge sorry notices)
• lake exe runLinter and lake exe lint-style for LeanPool, Challenge, and Solution
• python -m lean_pool.quality --repo ..
• pytest: 328 passed
• lake exe mk_all --check, local README/NOTICE regeneration checks (generated diffs omitted per PR policy), git diff --check, and forbidden-command scan
• #print axioms for covering_theorem, park_pham, and park_pham_bound: only propext, Classical.choice, Quot.sound

[Vilin97]

Import evidence review

Reviewed commit: ca59687c18e8f2b847fd44c31bf22148cf739916

1. Correctness and trust

• Both public wrapper theorems compile from a clean target build and the complete LeanPool aggregate build passes locally.
• The imported proof closure contains no sorry, admit, user axiom, unsafe, partial, opaque, native_decide, diagnostics, or local option overrides.
• #print axioms reports only [propext, Classical.choice, Quot.sound] for KahnKalai.covering_theorem, KahnKalai.park_pham, and the supporting park_pham_bound theorem.

2. Fidelity and sources

• Ported from dcposch/kahn-kalai-lean at 641aa75f, licensed Apache-2.0.
• The public theorem signatures are verbatim copies of the upstream challenge/solution surface. The implementation formalizes the Tran–Vu covering theorem with L = 1000 and the Park–Pham/Kahn–Kalai consequence with K = 100000, corresponding to Tran–Vu and Park–Pham. The catalog now states the covering result as its exact cross-multiplied cardinality inequality, noting that it is a density bound when the selected level is at most N and vacuous when the level exceeds N.
• Scope is stated narrowly: this import does not claim the optimized constant near 3.998, the Bell-number epsilon-covering refinement, or later sections of the Tran–Vu paper.

3. Quality and maintainability

• The upstream monolithic proof was split into Basic, Cost, Numeric, DoubleCount, Covering, and ParkPham, with a small public root module.
• Imports are precise, 18 public declarations have docstrings, the proof-size quality cap passes, and all upstream global heartbeat/linter overrides were removed. Four unused internal helper hypotheses reported by the first GPT review were also removed without changing the public theorem signatures.
• Local checks passed: runLinter, lint-style, python -m lean_pool.quality, lake exe mk_all --check, git diff --check, challenge build, and 328 pytest tests.

4. Novelty and significance

• The source completion commit is dated 2026-09-01 and falls inside the exact discovery window; no prior Lean Pool project, merged PR, open PR, or import-history entry matched it.
• It provides a reusable finite hypergraph expectation-threshold result and a formalized instance of the Kahn–Kalai conjecture proved by Park and Pham, rather than a benchmark scaffold or statement-only port.

5. Integration and performance

• The port builds on Lean Pool's Lean v4.34.0-rc1 environment from an upstream v4.32.0 source.
• In dependency-warm clean target builds, wall time improved from 20.68s to 16.09s (-22.2%), peak RSS from 3.61 GB to 2.87 GB (-20.5%), and jobs from 3,123 to 2,216 (-29.0%) after import tightening and proof restructuring.
• This PR intentionally contains only project content and registry wiring. Generated README.md/NOTICE changes are omitted because repository policy assigns them to the metadata workflow.

Verdict: merge-ready provided the fresh CI run and independent automated reviews are green with no material findings.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 42.71 s (= 0.71 min) — user 44.60 s, sys 5.59 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 589 maxHeartbeats units across 7 files (2,787 added LOC).

Sum of lean --profile: 34711.9 ms (= 34.71 s). Import-excluded time: 28576.9 ms (= 28.58 s).

Count-heartbeats wall-clock total: 38.06 s. Repeated import cost inside lean --profile: 6135.0 ms (= 6.13 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/KahnKalai/Cost.lean	378	189	3.29	2.69	1.70	0.99	45	0
LeanPool/KahnKalai/ParkPham.lean	729	132	7.38	8.20	7.12	1.08	33	0
LeanPool/KahnKalai/Covering.lean	786	84	10.03	13.08	12.07	1.01	21	0
LeanPool/KahnKalai/Basic.lean	198	76	3.16	2.05	1.05	1.00	19	0
LeanPool/KahnKalai/DoubleCount.lean	387	68	4.13	2.53	2.53	0.00	17	0
LeanPool/KahnKalai/Numeric.lean	261	36	6.61	4.85	3.87	0.98	18	0
LeanPool/KahnKalai.lean	48	4	3.46	1.31	0.24	1.07	2	0
Total	2,787	589	38.06	34.71	28.58	6.13	155	0

Aggregate phase totals

Phase	Time
typeclass inference	7502.1 ms (= 7.50 s)
interpretation	6436.0 ms (= 6.44 s)
import	6135.0 ms (= 6.13 s)
simp	3977.2 ms (= 3.98 s)
tactic execution	3447.0 ms (= 3.45 s)
norm_num	2778.1 ms (= 2.78 s)
type checking	958.4 ms (= 0.96 s)
elaboration	804.9 ms (= 0.80 s)
tacticAnalysis	565.9 ms (= 0.57 s)
ring	495.0 ms (= 0.49 s)
linting	479.9 ms (= 0.48 s)
initialization	232.8 ms (= 0.23 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.KahnKalai.Numeric	10.00 s
LeanPool.KahnKalai.Basic	9.70 s
LeanPool.KahnKalai.ParkPham	7.10 s
LeanPool.KahnKalai.Covering	6.60 s
LeanPool.KahnKalai.DoubleCount	2.40 s
LeanPool.KahnKalai.Cost	1.90 s
LeanPool.KahnKalai	1.40 s

Per-file `lean --profile` output

LeanPool/KahnKalai.lean

import took 1.07s
cumulative profiling times:
	attribute application 0.0256ms
	elaboration 12.5ms
	fix level params 0.0732ms
	import 1.07s
	initialization 36.5ms
	instantiate metavars 0.0532ms
	interpretation 169ms
	let-to-have transformation 0.0455ms
	linting 1.92ms
	module linting 0.00169ms
	overlappingInstancesLinter 2.69ms
	parsing 1.81ms
	process pre-definitions 0.441ms
	share common exprs 0.246ms
	tacticAnalysis 5.04ms
	type checking 1.19ms
	typeclass inference 11.1ms
real 1.80
user 1.19
sys 0.65

LeanPool/KahnKalai/Basic.lean

import took 1s
cumulative profiling times:
	attribute application 0.174ms
	blocked (unaccounted) 22.6ms
	compilation (IR) 0.264ms
	compilation (LCNF base) 3.95ms
	compilation (LCNF impure) 1.26ms
	compilation (LCNF mono) 2.29ms
	congr simp thm 1.71ms
	dsimp 2.45ms
	elaboration 55.5ms
	fix level params 1.23ms
	import 1s
	initialization 31.1ms
	instantiate metavars 1.67ms
	interpretation 292ms
	let-to-have transformation 0.162ms
	linting 25.7ms
	module linting 0.00179ms
	norm_num 0.421ms
	overlappingInstancesLinter 12.5ms
	parsing 13.6ms
	process pre-definitions 9.39ms
	ring 3.69ms
	share common exprs 3.49ms
	simp 128ms
	tactic execution 132ms
	tacticAnalysis 34.1ms
	type checking 23.9ms
	typeclass inference 246ms
real 2.13
user 1.92
sys 0.60

LeanPool/KahnKalai/Cost.lean

import took 990ms
cumulative profiling times:
	attribute application 0.613ms
	blocked (unaccounted) 4.55ms
	compilation (IR) 0.208ms
	compilation (LCNF base) 1.46ms
	compilation (LCNF impure) 0.933ms
	compilation (LCNF mono) 1.97ms
	congr simp thm 6.73ms
	elaboration 189ms
	fix level params 3.87ms
	import 990ms
	initialization 31.1ms
	instantiate metavars 3.2ms
	interpretation 480ms
	let-to-have transformation 0.541ms
	linting 65.3ms
	module linting 0.00193ms
	norm_num 1.55ms
	overlappingInstancesLinter 21.4ms
	parsing 23.5ms
	process pre-definitions 17.8ms
	ring 29.5ms
	share common exprs 11ms
	simp 69.2ms
	tactic execution 218ms
	tacticAnalysis 69.3ms
	type checking 84.6ms
	typeclass inference 364ms
real 2.07
user 2.58
sys 0.60

LeanPool/KahnKalai/Covering.lean

import took 1.01s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 123ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 396ms
simp took 751ms
cumulative profiling times:
	attribute application 0.348ms
	compilation (IR) 0.133ms
	compilation (LCNF base) 0.911ms
	compilation (LCNF impure) 0.667ms
	compilation (LCNF mono) 1.13ms
	congr simp thm 50.1ms
	elaboration 211ms
	fix level params 7.87ms
	import 1.01s
	initialization 31.1ms
	instantiate metavars 17.6ms
	interpretation 2.27s
	let-to-have transformation 1.63ms
	linting 165ms
	module linting 0.00169ms
	norm_num 1.6s
	overlappingInstancesLinter 17ms
	parsing 64.9ms
	process pre-definitions 67.7ms
	ring 188ms
	share common exprs 69.9ms
	simp 2.36s
	tactic execution 1.29s
	tacticAnalysis 173ms
	type checking 329ms
	typeclass inference 3.15s
real 6.17
user 12.88
sys 0.65

LeanPool/KahnKalai/DoubleCount.lean

import took 1e+03ms
cumulative profiling times:
	attribute application 0.223ms
	congr simp thm 4.52ms
	elaboration 89ms
	fix level params 2.91ms
	import 1e+03ms
	initialization 30.6ms
	instantiate metavars 4.25ms
	interpretation 595ms
	let-to-have transformation 0.294ms
	linting 66.7ms
	module linting 0.00143ms
	norm_num 33.1ms
	overlappingInstancesLinter 10.5ms
	parsing 26.4ms
	process pre-definitions 19ms
	ring 29.5ms
	share common exprs 12.3ms
	simp 241ms
	tactic execution 508ms
	tacticAnalysis 78ms
	type checking 99.7ms
	typeclass inference 681ms
real 2.45
user 3.40
sys 0.63

LeanPool/KahnKalai/Numeric.lean

import took 985ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 119ms
cumulative profiling times:
	attribute application 0.218ms
	congr simp thm 7.18ms
	elaboration 75.9ms
	fix level params 2.33ms
	import 985ms
	initialization 37.9ms
	instantiate metavars 4.61ms
	interpretation 1.03s
	let-to-have transformation 0.346ms
	linting 43.3ms
	module linting 0.00167ms
	norm_num 474ms
	overlappingInstancesLinter 6.69ms
	parsing 22ms
	process pre-definitions 26.9ms
	ring 85.3ms
	share common exprs 30.9ms
	simp 384ms
	tactic execution 323ms
	tacticAnalysis 57.5ms
	type checking 185ms
	typeclass inference 1.07s
real 3.04
user 4.70
sys 0.64

LeanPool/KahnKalai/ParkPham.lean

import took 1.08s
cumulative profiling times:
	attribute application 0.438ms
	blocked (unaccounted) 0.94ms
	compilation (IR) 0.115ms
	compilation (LCNF base) 2.55ms
	compilation (LCNF impure) 0.436ms
	compilation (LCNF mono) 0.882ms
	congr simp thm 23ms
	elaboration 172ms
	fix level params 4.32ms
	import 1.08s
	initialization 34.5ms
	instantiate metavars 13.7ms
	interpretation 1.6s
	let-to-have transformation 0.48ms
	linting 112ms
	module linting 0.00172ms
	norm_num 669ms
	overlappingInstancesLinter 18.2ms
	parsing 55.2ms
	process pre-definitions 59.3ms
	ring 159ms
	share common exprs 58.7ms
	simp 795ms
	tactic execution 976ms
	tacticAnalysis 149ms
	type checking 235ms
	typeclass inference 1.98s
real 5.18
user 8.04
sys 0.68

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[greptile-apps]

Greptile Summary

The PR imports the Kahn–Kalai expectation-threshold formalization and exposes its covering and Park–Pham headline theorems.

• Adds the seven-module Kahn–Kalai development and aggregate imports.
• Registers the project, source revision, provenance, and two main results.
• The current catalog and theorem docstring fully address the previously reported missing covering hypotheses.

Important Files Changed

Filename	Overview
LeanPool/KahnKalai.lean	Exposes both headline declarations; the covering theorem’s documentation now accurately states all formal hypotheses and boundary qualifications.
LeanPool/projects.yml	Registers the project and now describes the covering theorem consistently with its exact Lean declaration.
LeanPool/KahnKalai/Basic.lean	Introduces the finite-family, cover-cost, threshold, boundedness, and covering-level foundations used by the headline results.
LeanPool/KahnKalai/Cost.lean	Develops the cover-cost and restricted-family machinery supporting the covering argument.
LeanPool/KahnKalai/Covering.lean	Formalizes the quantitative Tran–Vu covering theorem used by the public headline declaration.
LeanPool/KahnKalai/ParkPham.lean	Derives the Park–Pham expectation-threshold bound with the advertised explicit witness.
LeanPool.lean	Adds the Kahn–Kalai project modules to the aggregate library import.

_{Reviews (6): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[github-actions]

🤖 LLM review (gpt-5.6-sol, 5 rubrics)

Reviewed head: 8887febd73999f98377ecf635af9da39745bce34

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Both headline declarations match their card informals, including the finite-ground-set regime and the explicit witnesses 1000 and 100000.
Novelty	✅ pass	Neither headline is already formalized by the supplied Mathlib hits or any listed pool project.
Significance	✅ pass	This is a completed research-level formalization of the Kahn–Kalai expectation-threshold theorem with a substantial supporting theory.
Sources	✅ pass	The citation and theorem-number attributions are internally consistent and the upstream Lean formalization is credited by repository and commit, but the paper’s exact hypotheses and constants are not verifiable from the diff alone.
Code quality (advisory)	✅ pass	The development is split into focused modules, and the long covering and threshold arguments are factored through named combinatorial, numeric, and measure lemmas rather than monolithic tactic scripts.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The covering theorem assumes ℓ ≤ Fintype.card α, 0 ≤ p, p ≤ 1, IsBounded H ℓ, and the stated lower bound on coverCost p H; the Park–Pham theorem assumes 2 ≤ ℓ and IsBounded F ℓ. All are disclosed in the card.
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	research
Branch	probabilistic combinatorics
Mode	theory_building
Code quality	4 / 5

Statement check: KahnKalai.covering_theorem proves the stated level-cardinality bound at coveringLevel, and KahnKalai.park_pham proves the universal threshold inequality with witness parkPhamK = 100000.

The contribution proves the quantitative Tran–Vu covering theorem as KahnKalai.covering_theorem and derives the named Park–Pham/Kahn–Kalai threshold bound as KahnKalai.park_pham.

---

Tokens: 290,972 in / 10,037 out across 5 rubric calls · Tier: flex / standard · Effort: xhigh · Cost: $1.0727
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

The first GPT review evaluated pre-fix SHA 4124610d. Its blocking faithfulness finding is fixed in 7aa302ed and accepted by Greptile’s fresh review. Its four advisory unused-hypothesis findings are fixed in 56d3f653; public theorem signatures are unchanged. Local target build, full Lean lint/style, repository quality, mk_all --check, diff/trust scans, and 327 applicable pytest tests pass.

[Vilin97]

Addressed the final GPT faithfulness finding in 5b09f3fb: both the public docstring and project catalog now state the exact cross-multiplied cardinality inequality, identify the m ≤ N density interpretation, and disclose that both cardinalities vanish when N < m. The theorem signature and proof are unchanged. Local build, Lean lint/style, repository quality, mk_all --check, diff checks, and 327 applicable pytest tests pass.