Twelve FATE-X formalizations diverge from their informal statements (compiling refutations included)

[Mariam581321]

While running agents against FATE-X I noticed that for some problems they consistently refused to believe the statement and instead formalised counterexamples. Claude helped me to scan the files and find the problems where the agents were correct. I also looked at the problems which were suspiciously easy to solve and found some where the formal statement is easier than the informal one. FATE-X 13, 23, 60, 75 are false as formalised, while 2, 15, 22, 59, 63, 81, 92, 96 are weaker than the informal statement (possibly on purpose in some cases but some look like genuine typos). Below suggested fixes per problem:

fatex_2

The formal statement is provable but is different (and easier) than the informal. The issue here is that IsMin is taken over the lattice of all normal subgroups, while in the informal statement we require minimal among all non-trivial normal subgroups.

Compiling proof that the conclusion set is always {⊥}

The current formalization makes the problem quite easy as the agents just prove that ⊥ is the only normal subgroup satisfying IsMin hence there are at most two of them. In lean:

import Mathlib

theorem minimal_normal_set_is_singleton_bot (G : Type) [Group G] :
    {H : {H : Subgroup G // H.Normal} | IsMin H}.ncard = 1 := by
  have hbot : (⊥ : Subgroup G).Normal := inferInstance
  let t : {H : Subgroup G // H.Normal} := ⟨⊥, hbot⟩
  have hle : ∀ H : {H : Subgroup G // H.Normal}, t ≤ H := by
    intro H; change (⊥ : Subgroup G) ≤ (H : Subgroup G); exact bot_le
  have hset : {H : {H : Subgroup G // H.Normal} | IsMin H} = {t} := by
    ext H
    constructor
    · intro hH; exact le_antisymm (hH (hle H)) (hle H)
    · rintro rfl; intro b _; exact hle b
  rw [hset]; exact Set.ncard_singleton t

The fix is to write {H : Subgroup G // H.Normal ∧ H ≠ ⊥} in the conclusion of the statement.

fatex_13

The formal statement is false (compiling counterexample in details). The informal "R is not a field" was rendered as ¬ IsField R, while the actual meaning was “R is not a division ring” because the informal statement explicitly says "R (not necessarily commutative) ring". Mathlib's IsField includes mul_comm, so the hypothesis is free for every noncommutative ring. This matters because the proof needs it to produce a nonzero non-invertible element; a ring failing only commutativity provides no such element (quaternions are a witness, formalised counterexample below).

Compiling refutation (Mathlib v4.27.0)

import Mathlib

open Quaternion

-- fatex_13 (FATE-X, FATEX/13.lean):
--   {R : Type} [Ring R] (h : ¬ IsField R) (h2 : ∀ x : R, ¬ IsUnit x → x^2 = x) (x : R) : x^2 = x
--
-- Witness: R = ℍ (Hamilton quaternions over ℝ).  ℍ is a *division ring*, so its only
-- non-unit is 0 and h2 holds vacuously; but Mathlib's `IsField` demands commutativity,
-- so `¬ IsField ℍ` also holds — and i² = -1 ≠ i.

/-- Mathlib's `IsField` includes `mul_comm`, so the noncommutative ℍ is not an `IsField`. -/
theorem not_isField_quaternion : ¬ IsField ℍ[ℝ] := by
  intro h
  have hc := h.mul_comm ⟨0, 1, 0, 0⟩ ⟨0, 0, 1, 0⟩   -- i * j = k,  j * i = -k
  norm_num [Quaternion.ext_iff, Quaternion.re_mul, Quaternion.imI_mul,
    Quaternion.imJ_mul, Quaternion.imK_mul] at hc

/-- In a division ring the only non-unit is 0, so fatex_13's hypothesis `h2` is vacuous. -/
theorem quaternion_h2 : ∀ x : ℍ[ℝ], ¬ IsUnit x → x ^ 2 = x := by
  intro x hx
  have : x = 0 := by
    by_contra hx0
    exact hx (isUnit_iff_ne_zero.mpr hx0)
  simp [this]

/-- But the conclusion fails: i² = -1 ≠ i. -/
theorem quaternion_i_sq : (⟨0, 1, 0, 0⟩ : ℍ[ℝ]) ^ 2 ≠ (⟨0, 1, 0, 0⟩ : ℍ[ℝ]) := by
  norm_num [pow_two, Quaternion.ext_iff, Quaternion.re_mul, Quaternion.imI_mul,
    Quaternion.imJ_mul, Quaternion.imK_mul]

/-- Hence the fatex_13 statement, quantified as written, is refutable. -/
theorem fatex13_false :
    ¬ ∀ (R : Type) [Ring R], ¬ IsField R → (∀ x : R, ¬ IsUnit x → x ^ 2 = x) →
      ∀ x : R, x ^ 2 = x := by
  intro H
  exact quaternion_i_sq (H ℍ[ℝ] not_isField_quaternion quaternion_h2 ⟨0, 1, 0, 0⟩)

#print axioms fatex13_false

The fix is to write ¬ (Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x) instead of ¬ IsField R.

fatex_15

The formal statement is vacuously true. The issue is in the setup structure Subgroup.IsMaximalNormal, which only requires H₁ ≤ H₂, and not a strict inclusion. This implies any RelSeries can be lengthened by repeating its last element, while NormalSubgroupCompositionSeries demands a series of maximum length among all series, so no such series can exist.

Compiling proof that the type is empty (Mathlib v4.27.0)

import Mathlib

-- Definitions copied verbatim from FATEX/15.lean:
structure Subgroup.IsMaximalNormal {G : Type} [Group G] (H₁ H₂ : Subgroup G) : Prop where
  le : H₁ ≤ H₂
  subgroupOf_normal : (H₁.subgroupOf H₂).Normal
  is_maximal : ∀ H : Subgroup G, H₁ ≤ H → H ≤ H₂ → (H.subgroupOf H₂).Normal → (H = H₁ ∨ H = H₂)

def Subgroup.IsMaximalNormal.setRel {G : Type} [Group G] : SetRel (Subgroup G) (Subgroup G) :=
  fun (H₁, H₂) ↦ Subgroup.IsMaximalNormal H₁ H₂

structure NormalSubgroupCompositionSeries (G : Type) [Group G] : Type where
  toRelSeries : RelSeries (Subgroup.IsMaximalNormal.setRel (G := G))
  maximal : ∀ s : RelSeries (Subgroup.IsMaximalNormal.setRel (G := G)),
      s.length ≤ toRelSeries.length

-- The relation is reflexive, so every series can be lengthened by repeating its last
-- element: no maximum-length series exists, and the type is empty for every group.
theorem composition_series_type_is_empty (G : Type) [Group G] :
    IsEmpty (NormalSubgroupCompositionSeries G) := by
  constructor
  intro Hs
  have rel : (Hs.toRelSeries.last, Hs.toRelSeries.last) ∈
      Subgroup.IsMaximalNormal.setRel (G := G) := by
    constructor
    · exact le_rfl
    · rw [Subgroup.subgroupOf_self]; exact Subgroup.Normal.mk (by intro n _ g; trivial)
    · intro H' hle1 hle2 _; left; exact le_antisymm hle2 hle1
  have hmax := Hs.maximal (Hs.toRelSeries.snoc Hs.toRelSeries.last rel)
  rw [RelSeries.snoc_length Hs.toRelSeries Hs.toRelSeries.last rel] at hmax
  omega

#print axioms composition_series_type_is_empty

The fix is to require H₁ < H₂ in IsMaximalNormal.

fatex_22

The formal statement is provable but strictly weaker than the informal. In the conclusion, we have ∃ n, x ^ n = 1 quantifying over n : ℕ, so n = 0 satisfies it making every x a "root of unity". The theorem reduces to the finiteness claim, so the problem is still nontrivial. The fix is to write ∃ n, 0 < n ∧ x ^ n = 1.

fatex_23

As stated the formalization is false (Lean counterexample in details). Notice that the problem statement doesn't hold for any non-zero constant polynomial (the numerator stays bounded while the denominator diverges, hence the limit is 0, not 1). The issue is that some constant polynomials are not excluded by the irreducibility condition (consider $f(x)=\pm p$ for a prime $p$, irreducible in $\mathbb{Z}[x]$). Adding 0 < f.natDegree restores the problem.

Compiling refutation (Mathlib v4.27.0)

import Mathlib
namespace Fatex23Probe

local instance (p : Nat.Primes) : NeZero p.1 := ⟨p.2.ne_zero⟩
local instance (p : Nat.Primes) : IsDomain (ZMod p) := @ZMod.instIsDomain p ⟨p.2⟩

/-- The benchmark statement, universally closed over `f`. -/
def Statement : Prop :=
  ∀ (f : Polynomial ℤ), Irreducible f →
    Function.rightLim
    (fun (s : ℝ) ↦
    (tsum (fun p : Nat.Primes ↦ (f.rootSet (ZMod p)).ncard * ((p : ℝ) ^ (-s)))) /
    (tsum (fun p : Nat.Primes ↦ (p : ℝ) ^ (-s)))) 1 = 1

/-- `2` is irreducible in `ℤ[X]`: it is `C 2` and `2` is prime in `ℤ`. -/
theorem irreducible_two : Irreducible (2 : Polynomial ℤ) := by
  have h2 : (2 : Polynomial ℤ) = Polynomial.C (2 : ℤ) := by norm_num
  rw [h2]
  exact (Polynomial.prime_C_iff.mpr Int.prime_two).irreducible

/-- A constant polynomial has no roots in any `ZMod p` (including `p = 2`, where it maps
to the zero polynomial and `roots 0 = 0`). -/
theorem rootSet_two_empty (p : Nat.Primes) :
    ((2 : Polynomial ℤ).rootSet (ZMod p)).ncard = 0 := by
  unfold Polynomial.rootSet
  rw [Polynomial.aroots]
  have h2 : (2 : Polynomial ℤ) = Polynomial.C (2 : ℤ) := by norm_num
  rw [h2, Polynomial.map_C, Polynomial.roots_C]
  simp

/-- Hence the whole ratio is the constant function `0`. -/
theorem ratio_two_eq_zero : (fun (s : ℝ) ↦
    (tsum (fun p : Nat.Primes ↦ ((2 : Polynomial ℤ).rootSet (ZMod p)).ncard * ((p : ℝ) ^ (-s)))) /
    (tsum (fun p : Nat.Primes ↦ (p : ℝ) ^ (-s)))) = fun _ : ℝ => 0 := by
  funext s
  have hnum : (tsum (fun p : Nat.Primes ↦
      ((2 : Polynomial ℤ).rootSet (ZMod p)).ncard * ((p : ℝ) ^ (-s)))) = 0 := by
    calc (tsum (fun p : Nat.Primes ↦
            ((2 : Polynomial ℤ).rootSet (ZMod p)).ncard * ((p : ℝ) ^ (-s))))
        = (tsum (fun _ : Nat.Primes => (0 : ℝ))) := by
          refine tsum_congr ?_
          intro p
          simp [rootSet_two_empty p]
      _ = 0 := by simp
  simp [hnum]

theorem rightLim_two_eq_zero : Function.rightLim
    (fun (s : ℝ) ↦
    (tsum (fun p : Nat.Primes ↦ ((2 : Polynomial ℤ).rootSet (ZMod p)).ncard * ((p : ℝ) ^ (-s)))) /
    (tsum (fun p : Nat.Primes ↦ (p : ℝ) ^ (-s)))) 1 = 0 := by
  rw [ratio_two_eq_zero]
  refine rightLim_eq_of_tendsto ?_ tendsto_const_nhds
  have hcl : (1 : ℝ) ∈ closure (Set.Ioi (1 : ℝ)) := by
    rw [closure_Ioi' (by simp : (Set.Ioi (1 : ℝ)).Nonempty)]
    simp
  exact (mem_closure_iff_nhdsWithin_neBot.mp hcl).ne'

/-- The benchmark statement is false. -/
theorem fatex23_false : ¬ Statement := by
  intro h
  have h2 := h 2 irreducible_two
  rw [rightLim_two_eq_zero] at h2
  exact absurd h2 (by norm_num)

#print axioms fatex23_false

end Fatex23Probe

fatex_59

The formal statement is strictly weaker than the informal. The informal asks to show that $v$ is a valuation with value group $\mathbb{Z} + \mathbb{Z}\alpha$ while the formalization asserts only the unique existence of an AddValuation satisfying the formula but without the value-group claim. The fix is to add it.

fatex_60

(The diagnosis below is entirely Claude's, I haven't verified the maths myself for this one.)

associatedPrimes expects a module, so associatedPrimes R I is read as the associated primes of the ideal-as-module ↥I, not the intended $\mathrm{Ass}(R/I)$. The informal statement's own parenthetical ("no associated primes at all — that is, when $I = R$") is true for $\mathrm{Ass}(R/I)$ and false for ↥I, which pins the intended reading. As written, the RHS is vacuously true at $I = \bot$ while Invertible ⊥ is false by definition — refuted with $R = \mathbb{Z}$, $I = \bot$. Independently, "codimension 1" was rendered as ringKrullDim (R ⧸ p) = 1, which is the dimension of $R/p$, not the codimension $\mathrm{ht}(p)$ — so fixing only the first issue still leaves a false statement, refuted with $R = \mathbb{Z}$, $I = (2)$: invertible, associated prime $(2)$ of codimension 1, but $\dim(\mathbb{Z}/(2)) = 0$.

Compiling refutations of both readings (Mathlib v4.27.0)

import Mathlib

namespace Fatex60Probe

/-- Verbatim from the benchmark file. -/
def Ideal.Invertible {R : Type} [CommRing R] [IsDomain R] (I : Ideal R) : Prop :=
    I ≠ ⊥ ∧ ∃ (N : Ideal R), (N * I).IsPrincipal ∧ N ≠ ⊥

/-- The benchmark's right-hand side elaborates to the associated primes of `I`
*as a module* (`↥I`), not of `R ⧸ I`. -/
example (R : Type) [CommRing R] (I : Ideal R) :
    associatedPrimes R I = associatedPrimes R ↥I := rfl

/-- ℤ satisfies the "locally factorial" hypothesis: it is a PID, hence Dedekind, so the
localization at each maximal ideal is a DVR, hence a UFD. -/
theorem int_h_ufd : ∀ (p : Ideal ℤ), (_ : p.IsMaximal) →
    UniqueFactorizationMonoid (Localization.AtPrime p) := by
  intro p hp
  haveI : p.IsPrime := hp.isPrime
  have hp0 : p ≠ ⊥ := by
    rintro rfl
    have hspan : (⊥ : Ideal ℤ) = Ideal.span {(2 : ℤ)} := by
      refine hp.eq_of_le ?_ bot_le
      intro htop
      rw [Ideal.span_singleton_eq_top, Int.isUnit_iff] at htop
      omega
    have : (2 : ℤ) ∈ (⊥ : Ideal ℤ) := hspan ▸ Ideal.mem_span_singleton_self 2
    simp at this
  haveI : IsDiscreteValuationRing (Localization.AtPrime p) :=
    IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain ℤ hp0 _
  infer_instance

/-- The zero ideal has no associated primes *as a module* (it is the zero module), so the
right-hand side holds vacuously — while `Invertible ⊥` is false by definition. -/
theorem bot_rhs_vacuous :
    ∀ (p : associatedPrimes ℤ ↥(⊥ : Ideal ℤ)), ringKrullDim (ℤ ⧸ p.1) = 1 := by
  rintro ⟨p, hp⟩
  exact absurd hp (not_isAssociatedPrime_of_subsingleton)

/-- Hence fatex_60, quantified as written, is refutable: take `R = ℤ`, `I = ⊥`. -/
theorem fatex60_false :
    ¬ ∀ (R : Type) [CommRing R] [IsDomain R] [IsNoetherianRing R],
        (∀ (p : Ideal R), (_ : p.IsMaximal) → UniqueFactorizationMonoid (Localization.AtPrime p)) →
        ∀ (I : Ideal R), Ideal.Invertible I ↔
          ∀ (p : associatedPrimes R I), ringKrullDim (R ⧸ p.1) = 1 := by
  intro H
  exact ((H ℤ int_h_ufd ⊥).mpr bot_rhs_vacuous).1 rfl

/-! ### Second, independent defect: "codimension 1" is rendered as a *co*height

`ringKrullDim (R ⧸ p)` is dim(R/p), not the codimension ht(p) = dim R_p.  So even after
replacing `associatedPrimes R I` by `associatedPrimes R (R ⧸ I)` the statement is still
false: over ℤ the invertible ideal (2) has Ass(ℤ/(2)) = {(2)}, of codimension 1, but
`ringKrullDim (ℤ ⧸ (2)) = dim 𝔽₂ = 0`. -/

theorem span_two_isPrime : (Ideal.span {(2 : ℤ)}).IsPrime :=
  (Ideal.span_singleton_prime (by norm_num)).mpr Int.prime_two

theorem span_two_invertible : Ideal.Invertible (Ideal.span {(2 : ℤ)}) := by
  refine ⟨?_, ⊤, ?_, top_ne_bot⟩
  · simp [Ideal.span_singleton_eq_bot]
  · rw [Ideal.top_mul]
    exact ⟨2, rfl⟩

theorem ass_quot_span_two :
    associatedPrimes ℤ (ℤ ⧸ Ideal.span {(2 : ℤ)}) = {Ideal.span {(2 : ℤ)}} := by
  rw [associatedPrimes.eq_singleton_of_isPrimary span_two_isPrime.isPrimary,
    span_two_isPrime.radical]

/-- Fixing only the `associatedPrimes` bug is not enough: the resulting statement is
still refuted by `R = ℤ`, `I = (2)`. -/
theorem coheight_reading_still_false :
    ¬ (Ideal.Invertible (Ideal.span {(2 : ℤ)}) ↔
        ∀ p ∈ associatedPrimes ℤ (ℤ ⧸ Ideal.span {(2 : ℤ)}), ringKrullDim (ℤ ⧸ p) = 1) := by
  intro h
  have hdim := h.mp span_two_invertible (Ideal.span {(2 : ℤ)}) (by rw [ass_quot_span_two]; rfl)
  haveI : (Ideal.span {(2 : ℤ)}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible Int.prime_two.irreducible
  have hfield : IsField (ℤ ⧸ Ideal.span {(2 : ℤ)}) :=
    (Ideal.Quotient.maximal_ideal_iff_isField_quotient _).mp inferInstance
  rw [ringKrullDim_eq_zero_of_isField hfield] at hdim
  exact absurd hdim (by decide)

#print axioms fatex60_false
#print axioms coheight_reading_still_false

end Fatex60Probe

The suggested fix is ∀ p ∈ associatedPrimes R (R ⧸ I), p.height = 1 in place of ∀ (p : associatedPrimes R I), ringKrullDim (R ⧸ p.1) = 1, which restores the intended exercise.

fatex_63

The formal statement is provable but different (and easier) than the informal. The informal statement asks for a surjection of $R$-algebras $S' \to S$ with square-zero kernel and the universal lifting property, but the formalization never requires f to be surjective. In particular if we don't require surjectivity, [Algebra.FormallyUnramified R S] is not needed anymore. The details contain a compiling proof (an accepted solution produced by an agent during the benchmark) of the statement as formalized with that hypothesis deleted, so the problem as stated is solvable for an arbitrary $R$-algebra $S$.

Compiling proof with the FormallyUnramified hypothesis removed (Mathlib v4.27.0)

import Mathlib

namespace Fatex63Probe

def UniversalProperty.liftOfSqZeroIdeal {R S S' : Type} [CommRing R] [CommRing S] [CommRing S']
    [Algebra R S] [Algebra R S'] (f : S' →ₐ[R] S) :=
  ∀ (A : Type) [CommRing A] [Algebra R A] (I : Ideal A) (g : S →ₐ[R] A⧸I),
  I^2 = 0 → (g.toRingHom.comp (algebraMap R S) = (Ideal.Quotient.mk I).comp (algebraMap R A)) →
  ∃! (g' : S' →ₐ[R] A), (Ideal.Quotient.mk I).comp g'.toRingHom  = g.comp f

theorem hypothesis_unused (R S : Type) [CommRing R] [CommRing S]
    [Algebra R S] :
    ∃ (S' : Type) (_ : CommRing S') (_ : Algebra R S') (f : S' →ₐ[R] S), (RingHom.ker f) ^ 2 = 0 ∧ UniversalProperty.liftOfSqZeroIdeal f := by
  let f₀ : R →ₐ[R] S := IsScalarTower.toAlgHom R R S
  let J : Ideal R := RingHom.ker f₀.toRingHom
  refine ⟨R ⧸ J ^ 2, inferInstance, inferInstance, f₀.kerSquareLift, ?_, ?_⟩
  · -- kernel has square zero
    have hker : RingHom.ker f₀.kerSquareLift = J.cotangentIdeal := by
      simpa [J] using AlgHom.ker_kerSquareLift f₀
    rw [hker]
    exact Ideal.cotangentIdeal_square J
  · -- universal property
    intro A _ _ I g hI hcompat
    let a₀ : R →ₐ[R] A := IsScalarTower.toAlgHom R R A
    have hmemI : ∀ r : R, r ∈ J → a₀ r ∈ I := by
      intro r hr
      have hf0 : f₀ r = 0 := by
        simpa [J] using hr
      have hπ : (Ideal.Quotient.mk I) (a₀ r) = 0 := by
        have h := congrArg (fun φ : R →+* A ⧸ I => φ r) hcompat
        calc
          (Ideal.Quotient.mk I) (a₀ r) = (Ideal.Quotient.mk I) (algebraMap R A r) := by
            simp [a₀, IsScalarTower.toAlgHom_apply]
          _ = g.toRingHom (algebraMap R S r) := by
            simp
          _ = g.toRingHom (f₀ r) := by
            simp [f₀, IsScalarTower.toAlgHom_apply]
          _ = g.toRingHom 0 := by rw [hf0]
          _ = 0 := by simp
      rw [← sub_zero (a₀ r)]
      exact (Ideal.Quotient.mk_eq_mk_iff_sub_mem (a₀ r) 0).mp (by simpa using hπ)
    have hJ2 : ∀ r : R, r ∈ J ^ 2 → a₀ r = 0 := by
      intro r hr
      have hmapJ : Ideal.map a₀.toRingHom J ≤ I := by
        exact (Ideal.map_le_iff_le_comap).2 (by intro x hx; exact hmemI x hx)
      have hI2 : I * I = ⊥ := by
        rw [← pow_two]
        exact hI
      have hmapJ2 : Ideal.map a₀.toRingHom (J ^ 2) = ⊥ := by
        apply le_antisymm
        · rw [pow_two, Ideal.map_mul]
          exact le_trans (Ideal.mul_mono hmapJ hmapJ) (le_of_eq hI2)
        · exact bot_le
      have : a₀ r ∈ (⊥ : Ideal A) := by
        rw [← hmapJ2]
        exact Ideal.mem_map_of_mem a₀.toRingHom hr
      simpa using this
    let g' : (R ⧸ J ^ 2) →ₐ[R] A := Ideal.Quotient.liftₐ (J ^ 2) a₀ hJ2
    refine ⟨g', ?_, ?_⟩
    · -- the lift equation
      apply RingHom.ext
      intro x
      rcases Ideal.Quotient.mk_surjective x with ⟨r, rfl⟩
      calc
        (Ideal.Quotient.mk I).comp g'.toRingHom (Ideal.Quotient.mk (J ^ 2) r)
            = (Ideal.Quotient.mk I) (g' (Ideal.Quotient.mk (J ^ 2) r)) := by rfl
        _ = (Ideal.Quotient.mk I) (a₀ r) := by
          simp [g', Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
        _ = (Ideal.Quotient.mk I) (algebraMap R A r) := by
          simp [a₀, IsScalarTower.toAlgHom_apply]
        _ = g.toRingHom (algebraMap R S r) := by
          simp
        _ = g (f₀ r) := by
          simp [f₀, IsScalarTower.toAlgHom_apply]
        _ = g (f₀.kerSquareLift (Ideal.Quotient.mk (J ^ 2) r)) := by
          rw [AlgHom.kerSquareLift_mk f₀ r]
        _ = g.comp f₀.kerSquareLift (Ideal.Quotient.mk (J ^ 2) r) := by rfl
    · -- uniqueness
      intro g'' hg''
      apply AlgHom.ext
      intro x
      rcases Ideal.Quotient.mk_surjective x with ⟨r, rfl⟩
      calc
        g'' (Ideal.Quotient.mk (J ^ 2) r) = algebraMap R A r := by
          rw [← Ideal.Quotient.algebraMap_eq]
          exact g''.commutes r
        _ = g' (Ideal.Quotient.mk (J ^ 2) r) := by
          simp [g', Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk, a₀]

end Fatex63Probe
#print axioms Fatex63Probe.hypothesis_unused

The fix is to add Function.Surjective f to the existential.

fatex_75

The informal and formal statements agree but are incorrect as stated. Fable guessed the problem comes from Bruns W, Herzog HJ. Cohen-Macaulay Rings, and indeed I checked it is exactly 2.1.27(b), (i) ⟺ (iii), with $A = M = R$. Instead of $(A_p)_0$ (only the degree-zero part) we should have $(A_p)$. Fable gives $A = k[X,Y]/(X^2, XY)$ as a hand-verified counterexample claiming formalising is difficult with current Mathlib content.

The fix in lean is to swap HomogeneousLocalization.AtPrime 𝒜 p with Localization.AtPrime p and drop the $_0$ from the informal statement as well.

fatex_81

This one has wrong parentheses in the formalization: in Lean the body of ∃ extends to the end of the term, so the existential entails the whole iff instead of just its left side making the statement equivalent to only one direction of the intended iff (see details).

Compiling parse pin and one-direction equivalence (Mathlib v4.27.0)

import Mathlib

/-!
# fatex_81 (FATE-X, FATEX/81.lean) — a binder/precedence misformalization

Informal statement:
  "Let `A` be a local Noetherian ring, `I ⊂ A` an ideal.  Show that `I` is generated by a
   regular sequence **if and only if** `I/I²` is free over `A/I` and `pd_A I < ∞`."

So the intended Lean statement is

  (∃ rs, IsRegular R rs ∧ Ideal.ofList rs = I) ↔ (Free (R⧸I) I.Cotangent ∧ ∃ n, pd ≤ n)

but the benchmark file writes the existential **without parentheses**:

  ∃ (rs : List R), (IsRegular R rs) ∧ Ideal.ofList rs = I ↔ Free … ∧ (∃ n, …)

and in Lean the body of `∃` extends to the end of the term, so this parses as

  ∃ rs, ((IsRegular R rs ∧ Ideal.ofList rs = I) ↔ (Free … ∧ ∃ n, …))

i.e. the existential binds the *whole* iff.  Below: the parse is confirmed by `Iff.rfl`,
and the benchmark statement is proved **equivalent to a single implication** — the
"if" direction (Vasconcelos) only.  The "only if" direction of the informal statement
(a regular sequence forces `I/I²` free and `pd_A I < ∞`) is discarded: the witness `rs = [1]`
makes the iff vacuously true whenever the right-hand side fails, using only `I ≠ ⊤`.
-/

namespace Fatex81

open CategoryTheory

/-- The right-hand side of the benchmark iff (verbatim). -/
def RHS (R : Type) [CommRing R] (I : Ideal R) : Prop :=
  Module.Free (R ⧸ I) I.Cotangent ∧
    (∃ n, CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R I) n)

/-- The left-hand side of the benchmark iff, for a fixed list (verbatim). -/
def LHS (R : Type) [CommRing R] (I : Ideal R) (rs : List R) : Prop :=
  (RingTheory.Sequence.IsRegular R rs) ∧ Ideal.ofList rs = I

/-- The benchmark statement, copied verbatim from `FATEX/81.lean` (conclusion only). -/
def Benchmark (R : Type) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (I : Ideal R) : Prop :=
    ∃ (rs : List R), (RingTheory.Sequence.IsRegular R rs) ∧ Ideal.ofList rs = I ↔
    Module.Free (R ⧸ I) I.Cotangent ∧
    (∃ n, CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R I) n)

/-- The statement the informal text asks for. -/
def Intended (R : Type) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (I : Ideal R) : Prop :=
    (∃ (rs : List R), LHS R I rs) ↔ RHS R I

/-- **The parse.**  The benchmark's `∃` binds the entire `↔`; it is *not* an iff between
the existential and the right-hand side. -/
theorem benchmark_parse (R : Type) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (I : Ideal R) : Benchmark R I ↔ ∃ rs : List R, (LHS R I rs ↔ RHS R I) := Iff.rfl

/-- `Ideal.ofList [1] = ⊤`, so `[1]` never generates a proper ideal. -/
theorem ofList_one (R : Type) [CommRing R] : Ideal.ofList [(1 : R)] = ⊤ := by
  rw [Ideal.ofList_singleton, Ideal.span_singleton_one]

/-- **The collapse.**  Under the benchmark's own hypothesis `I ≠ ⊤`, the statement the
benchmark actually makes is *equivalent* to the single implication
`RHS → ∃ rs, rs is a regular sequence generating I` — the "if" half of the informal iff.
The "only if" half is not asserted at all. -/
theorem benchmark_iff_one_direction (R : Type) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] (I : Ideal R) (netop : I ≠ ⊤) :
    Benchmark R I ↔ (RHS R I → ∃ rs : List R, LHS R I rs) := by
  rw [benchmark_parse]
  constructor
  · rintro ⟨rs, h⟩ hR
    exact ⟨rs, h.mpr hR⟩
  · intro H
    by_cases hR : RHS R I
    · obtain ⟨rs, hrs⟩ := H hR
      exact ⟨rs, iff_of_true hrs hR⟩
    · refine ⟨[1], iff_of_false (fun ha => ?_) hR⟩
      exact netop ((ofList_one R).symm.trans ha.2).symm

/-- Consequently the benchmark statement is strictly implied by the intended one: anyone
who proves the informal theorem proves the benchmark, but not conversely — only the
`←` direction of `Intended` is ever needed. -/
theorem intended_implies_benchmark (R : Type) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] (I : Ideal R) (netop : I ≠ ⊤) :
    Intended R I → Benchmark R I := by
  intro h
  rw [benchmark_iff_one_direction R I netop]
  exact h.mpr

/-- And the discarded direction really is discarded: the benchmark follows from the
"if" half alone, with no use of the "only if" half. -/
theorem benchmark_of_backward_only (R : Type) [CommRing R] [IsLocalRing R]
    [IsNoetherianRing R] (I : Ideal R) (netop : I ≠ ⊤)
    (backward : RHS R I → ∃ rs : List R, LHS R I rs) :
    Benchmark R I :=
  (benchmark_iff_one_direction R I netop).mpr backward

/-! ### Why the `I ≠ ⊤` hypothesis is load-bearing

With the intended parenthesisation, `netop` is unnecessary: for `I = ⊤` both sides of the
informal iff are false-ish/true-ish in a way that is a theorem either way.  With the
benchmark's parse it is *required*: `Ideal.ofList rs = ⊤` contradicts `IsRegular`'s
`top_ne_smul` field, so `LHS R ⊤ rs` is false for every `rs`, while `RHS R ⊤` is true
(`⊤.Cotangent` is subsingleton and `ModuleCat.of R ↥⊤` is projective — *asserted, not
verified here*), which would make the statement false at `I = ⊤`. -/

theorem lhs_top_false (R : Type) [CommRing R] (rs : List R) : ¬ LHS R ⊤ rs := by
  rintro ⟨hreg, hgen⟩
  exact hreg.top_ne_smul (by rw [hgen]; simp)

#print axioms benchmark_parse
#print axioms benchmark_iff_one_direction
#print axioms intended_implies_benchmark
#print axioms lhs_top_false

end Fatex81

The fix is to parenthesize: (∃ (rs : List R), RingTheory.Sequence.IsRegular R rs ∧ Ideal.ofList rs = I) ↔ ….

fatex_92

The formal statement is strictly weaker than the informal. In the second half of the problem, we're asked to construct a ring realizing the sequence for all k : ℕ (∀ (k : ℕ), ∃ (A : Type) …) omitting the $k = \infty$ dimension sequence, which is present in the first half of the question. The fix is to quantify over k : ℕ∞.

fatex_96

The formal statement is strictly weaker than the informal. The guard h : ∀ n : ℕ, (f.eval (RingHom.id ℚ))^[n] a ≠ 0 is commented as excluding division by zero, but it also excludes orbits that legitimately pass through $0$ (when $0$ is not a pole of $f$), so the theorem is never asserted for them. The fix is to weaken the guard to exclude only actual poles, i.e. require that no iterate is a zero of f.denom.