All issues

Search results

ECHIDNA pipeline reports 15 known-good proofs "invalid" — provers invoked without project/library context

Status: Open.

#162In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jul 7, 2026

[Idris2] hardwareEraseIrreversible non-theorem-as-stated (RMO.idr:213-215)

Status: Open.

#130In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 2, 2026

[meta] decide on .github/copilot/coding-agent.yml MCP config (from stale-branch cruft 2026-06-02)

Status: Open.

#111In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 2, 2026

Tier-S: #45 sub — 10 remaining practice gaps (3-12, gap-per-PR)

Status: Open.

#94In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #45 Frontier 5 — Lean → Rust correspondence mechanization

Status: Open.

#93In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #45 Frontier 4 — GDPR / RMO completeness theory (BLOCKED on #60, #61)

Status: Open.

#92In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #45 Frontier 3 — POSIX 2024 conformance theory

Status: Open.

#91In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #45 Frontier 2 — concurrency / linearizability theory

Status: Open.

#90In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #41 sub — 28 TODO markers by hot-spot file (per-file PR)

Status: Open.

#88In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #41 sub — 3 production panic! sites (typed-error conversion)

Status: Open.

#87In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #41 sub — 10 unreachable! production sites (one PR per file)

Status: Open.

#86In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026

Tier-S: #43 sub — fuzz targets (7 → 20, +13)

Status: Open.

#85In Hyperpolymath/valence-shell;

· hyperpolymath opened on Jun 1, 2026