From e5cecac38823d5af8ab990e395e6b023ea98db9e Mon Sep 17 00:00:00 2001 From: openresearch Date: Sat, 4 Jul 2026 22:55:02 +0000 Subject: [PATCH] =?UTF-8?q?docs:=20update=20test=20matrix=20=E2=80=94=20C1?= =?UTF-8?q?=20FAIL,=20C2=20PARTIAL=20(HCMR=20builds,=20rest=20fail)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lake build results (run 019f2f3f, 24min, 8 vCPUs): - HCMR.lean: BUILT ✅ (agent fix worked — removed excess omega, downgraded false theorem from > to ≥) - CacheSieve.lean: FAILED ❌ (agent fix incomplete — still has errors) - Blitter6502OISC.lean: FAILED ❌ (type class synthesis L62, rewrite failures L135/L142) - YangMillsPerformance.lean: FAILED ❌ (10 errors — omega/linarith can't handle Nat.div, 1 sorry) - WorkloadTestbench.lean: NOT REACHED (depends on failed CacheSieve) - CRTSidonN.lean: FAILED ❌ (errors after agent fix) Root causes: - YangMills: proofs use omega/linarith for Nat.div goals (wrong tactic) - Blitter: type class instance missing, rw patterns don't match - CacheSieve: agent fix didn't fully resolve all issues - CRTSidonN: compilation errors remain For future builds: add 'lake exe cache get' before 'lake build' to download precompiled Mathlib oleans (saves ~20min). --- docs/research/COMPLETE_TEST_MATRIX.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/research/COMPLETE_TEST_MATRIX.md b/docs/research/COMPLETE_TEST_MATRIX.md index 4c6a63a4..73bc07c8 100644 --- a/docs/research/COMPLETE_TEST_MATRIX.md +++ b/docs/research/COMPLETE_TEST_MATRIX.md @@ -103,8 +103,8 @@ For each component of the framework, we ask: | Test | Question | Input | Prediction | Receipt | Status | |------|----------|-------|------------|---------|--------| -| T35 | Does CRTSidonN compile? | lake build | exit 0 | C1 | PENDING (build at 89%) | -| T36 | Does HCMR suite compile? | lake build | exit 0, 2 sorries | C2 | PENDING (same build) | +| T35 | Does CRTSidonN compile? | lake build | exit 0 | C1 | DONE: FAIL ❌ (errors after agent fix) | +| T36 | Does HCMR suite compile? | lake build | exit 0, 2 sorries | C2 | DONE: PARTIAL — HCMR ✅, CacheSieve ❌, Blitter ❌, YangMills ❌, WorkloadTestbench not reached | | T37 | Are the proven theorems non-tautological? | Review each proof | At least sidon_preserved_mod is non-trivial | Adversarial review | DONE: sidon_preserved (componentwise) is tautological, sidon_preserved_mod is real | | T38 | Does native_decide use violate AGENTS.md? | helical_coverage_74 | Uses native_decide | HopfFibration.lean | DONE: YES, uses native_decide (documented exception for finite decidability) |