From a591baeb8c0924bfef49be5b27d45e93d4634c53 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Mon, 15 Jun 2026 01:17:58 +0000 Subject: [PATCH] =?UTF-8?q?fix(lean):=20correct=20sorry=20inventory=20coun?= =?UTF-8?q?t=20in=20=C2=A712=20(10=20=E2=86=92=2012)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Allaun Silverfox --- 0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index d94d71fe..9dc041b4 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -417,7 +417,7 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) : |------|------|--------|--------| | `e8_additive_completeness` | §10 | axiom | Open problem in additive combinatorics | -### Sorry inventory (10 total, all with TODO(lean-port)) +### Sorry inventory (12 total, all with TODO(lean-port)) | Item | Line | Blocked on | |------|------|------------|