Repository navigation
Publish a research note on the shift-8 proof and causal diagnostic failure #2
Description
Summary
Write and publish a technical research note documenting the kernel-verified shift-8 classification and the debugging phenomenon uncovered during the proof search.
The central story is not merely that the theorem was proved. It is that the human proposed a software-bug hypothesis, the agent audited the assembly pipeline and rejected that hypothesis with evidence, then independently found the actual problem: mundane Lean proof issues whose diagnostics cascaded incorrectly through the compact reporting layer.
Core facts to cover
- Target:
(n - 8) / 8is prime or twice a prime. - Proof method: 2-adic odd-part decomposition,
Nat.exists_eq_two_pow_mul_odd,sigma_zero_apply_prime_pow, three-way split, and size-bound elimination of thea ≥ 2branch. - Twelve failed attempts prominently reported
No goals to be solved. - The assembly pipeline was investigated and found faithful.
- Async verification exposed the full ordered diagnostics.
- Root repairs included:
rw [...] <;> ringwhererwcould close by definitional equality;- restoring
hs1 : 1 ≤ s; - normalizing
2 ^ 1 * sto2 * sbeforeomega.
- The theorem was then kernel-verified.
- Follow-up issue:
llm-driven-proof-search#240, causal diagnostic summaries.
Required framing
- Avoid portraying the result as mystical autonomous discovery.
- Emphasize hypothesis testing between human, agent, source code, and verifier evidence.
- Distinguish the mathematical theorem from the systems finding.
- Explain why complete ordered diagnostics and repair trajectories are valuable training data.
- State clearly that diagnostic causality is heuristic metadata, not proof authority.
Suggested title
The Error Was Real, but the Diagnosis Was Wrong: A Forensic Lean Proof Search Case Study
Required links
- Proof Search repository
- Issue #240
- public proof dossier or redacted episode summary, where disclosure policy permits
- MathCorpus explanation of repair trajectories
- Mnemosyne Research Institute
Acceptance criteria
- New MD/MDX post appears in the blog index and RSS/feed if supported.
- Includes code snippets showing the cascade pattern and final repair.
- Includes a compact timeline from human hypothesis to kernel verification.
- Contains no unsupported novelty claim about the underlying mathematics.
- Metadata, social preview, tags, and canonical URL are complete.
npm run buildpasses.
Activity