Formalization session: Fermat's Last Theorem for 37

The problem

Fermat's Last Theorem for exponent 37 is settled mathematics. This simulated record treats its Lean target as open. Its pinned corpus contains small-exponent results and the regular-prime route, while exponent 37 falls outside that route because 37 is irregular.

The obstruction

The one formalized route is Kummer's descent in the cyclotomic ring ℤ[ζ₃₇]. The descent needs control over factorization there, and the class number h(ℚ(ζ₃₇)) measures the failure of unique factorization, so the argument carries the hypothesis 37 ∤ h.

For 37 the hypothesis is false: 37 divides h, which is whatirregular means. Every transport of the formal proof dies at that hypothesis. The simulated memory holds 212 such failed attempts and a summary of the shared obstruction.

Result produced by this session

Kummer's criterion turns irregularity into a finite computation: p is irregular exactly when p divides the numerator of a Bernoulli number B_k with even k ≤ p − 3. For 37 the witness is B₃₂. The session proves that witness, deposits it as pending verification, and leaves the theorem open with a sharper account of the obstruction.