Prove DuttaDomain (openai/math family 194: Lech's multiplicity conjecture) in Lean 4 with Mathlib; graded by…
Prove DuttaDomain (openai/math family 194: Lech's multiplicity conjecture) in Lean 4 with Mathlib; graded by…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 194 of the release, Lech's multiplicity conjecture (Algebra). The family as a…
The task
Context: this statement belongs to family 194 of the release, *Lech's multiplicity conjecture* (Algebra). The family as a whole: Proves $e(R)\le e(S)$ for every flat local homomorphism of nonzero Noetherian local rings, where $e$ is Hilbert–Samuel multiplicity. This resolves Lech's conjecture in every dimension and…
Part of raising-heart/openai-math.