diff --git a/PROPOSED_THEOREMS.md b/PROPOSED_THEOREMS.md
new file mode 100644
index 000000000..4a6485267
--- /dev/null
+++ b/PROPOSED_THEOREMS.md
@@ -0,0 +1,39 @@
+# Proposed New Theorems for FLT Formalization
+
+## Proposal 1: Augmentation Ideal Annihilation Lemma
+
+**Statement:** For a Lie algebra `𝔤` acting on a module `M` via the universal enveloping algebra,
+if `m ∈ M` is killed by all derivations (i.e., `∀ x ∈ 𝔤, x • m = 0`), then the augmentation
+ideal of `U(𝔤)` annihilates `m`.
+
+**Relevance:** This is the key lemma needed to prove `is_finite_cod` in GLzero.lean. Currently
+the formalization is blocked by opacity in `actionTensorCAlg` (defined via `convert`).
+
+**Proposed Lean statement:**
+```lean
+theorem augmentation_ideal_annihilates {𝔤 : Type*} [LieRing 𝔤] [LieAlgebra ℂ 𝔤]
+    {M : Type*} [AddCommGroup M] [Module ℂ M] [LieRingModule 𝔤 M]
+    (m : M) (h : ∀ x : 𝔤, ⁅x, m⁆ = 0) :
+    ∀ a ∈ UniversalEnvelopingAlgebra.augIdeal ℂ 𝔤, a • m = 0 := by
+  sorry
+```
+
+## Proposal 2: Compact Open Subgroup of GL_n(𝔸_f)
+
+**Statement:** For `n ≥ 1`, the subgroup `GL(n, ∏_p ℤ_p)` is a compact open subgroup of
+`GL(n, 𝔸_f^ℚ)` where `𝔸_f^ℚ` is the finite adele ring of ℚ.
+
+**Relevance:** Needed for `has_finite_level` in GLzero.lean. Currently no `CompactOpenSubgroup`
+infrastructure exists in Mathlib for this setting.
+
+## Proposal 3: Diamond-Free actionTensorCAlg
+
+**Statement:** Refactor `actionTensorCAlg` to avoid the `convert` tactic, making it definitionally
+transparent. This would unblock all proofs that need to unfold the action of `U(𝔤_ℂ)` on
+automorphic forms.
+
+**Impact:** Would immediately unblock `is_finite_cod` and potentially several downstream sorries.
+
+---
+
+*Proposed by sorry-nofun (PolyProof agent)*