Repository navigation
feat(abstracts): add readable communication and randomized-complexity headlines #492
Description
Add self-contained, readable formal abstracts for substantial proved headline results currently missing from the selected catalogue. Initial candidates are randomized communication lower bounds (disjointness, with the deterministic/randomized equality contrast) and Sipser–Lautemann / Karp–Lipton; select final groups after inspecting their exact sources. Preserve the small coherent selection, existing editorial exclusions and mathematical/formalization credit.
Completion: explicit conventional models and bounds in the public abstracts, checked bridge proofs and #check_abstract audits, imports/catalogue/build-guide updates, all six repository gates, rendering/tooling checks, inspected PDF pages and declaration links, and independent API/correctness/readability review of the final revision. Do not promote incomplete theorem substitutes. No changes to the underlying library theorem semantics.
Worker/session: abstracts-20261023-root (OpenAI Codex). Planned isolated branch feat/headline-abstracts-20261023. Read-only candidate survey delegated to /root/headline_survey; root owns all edits. This task implements Samuel's request to build abstracts for notable missing headline theorems, prioritizing readability for experts unfamiliar with Lean.
Activity
SamuelSchlesinger commentedon Oct 23, 2026
active — worker abstracts-20261023-root claims this task on
feat/headline-abstracts-20261023, isolated worktree.worktrees/headline-abstracts. Root owns edits;/root/headline_surveyis surveying candidate semantics read-only. First implementation will cover communication lower bounds, followed by the missing randomized-complexity headline after the source audit.SamuelSchlesinger commentedon Oct 23, 2026
active — worker abstracts-20261023-root: the communication and Sipser–Gács–Lautemann drafts and nonvacuity tests are prepared. Finishing the prerequisite source relocation in #497 first, as requested; then I will add these two groups in a separate stacked PR and validate the final Lean sources and rendered pages.
SamuelSchlesinger commentedon Oct 23, 2026
awaiting review — worker abstracts-20261023-root: #499 adds the communication and Sipser–Gács–Lautemann groups, stacked on relocation #497. Validation and local PDF/source-link review are recorded in the PR; independent exact-revision coordinator review requested. Both new PDFs are two pages; the broader library statements are unchanged.
SamuelSchlesinger commentedon Oct 24, 2026
Active refresh — worker
codex-review-559, delegated bycoordinator-codex-01a16ab8: refreshing #499 onto current main, preserving the original authors and prior mathematical/review evidence. Isolated branchrefresh/headline-abstracts-codex; original branches and remote heads remain intact. Scope is the original payload plus current canonical-name/plain-API and renderer integration adaptations, followed by all six gates and final hosted PDF/provenance review. No new mathematical claims or S1/Tactic changes.SamuelSchlesinger commentedon Oct 24, 2026
Awaiting independent delta review — worker
codex-review-559undercoordinator-codex-01a16ab8: refreshed #499 at4abdb895, preserving original authors and prior mathematical review. All six gates and focused Lean/renderer checks pass; the PR body owns the evidence and remaining exact hosted PDF/provenance inspection requirement. No new mathematical scope or author approval.