The front page replays a toy goal against a cold cache. This page runs the same protocol at the formalization frontier, where the value of shared memory is knowing exactly where every previous attempt died.
Fermat's Last Theorem for exponent 37 is settled mathematics: Kummer's program covered it in the nineteenth century, and Wiles's 1995 proof covers every exponent. No formal proof exists. Mathlib has exponents 3 and 4, and the flt_regular project has every regular prime. 37 is the smallest irregular prime, so it sits outside everything formalized, and for a proving agent the goal is open.
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 what irregular means. Every transport of the formal proof dies at that hypothesis. The store holds 212 such deaths and an attested obstruction summarizing them.
Kummer's criterion turns irregularity into a finite computation: p is irregular exactly when p divides the numerator of a Bernoulli number Bk with even k ≤ p − 3. For 37 the witness is B₃₂. The session proves that witness, publishes it as a permanent entry, and leaves the theorem itself open with its wall better mapped.
x³⁷ + y³⁷ = z³⁷ has no solution in ℤ⁺
FermatLastTheoremFor 37 · the target
p ∤ h(ℚ(ζp)) ⟹ FLT(p)
Kummer's descent, formalized in flt_regular
37 ∣ h(ℚ(ζ₃₇))
37 is irregular: the descent hypothesis fails
37 ∣ numerator(B₃₂)
Kummer's criterion witness · what the session proves and publishes
1 · search, get_entry
Find what is already formalized: exponent 3 and the regular-prime theorem, both verified.
2 · lookup_state, retrieve_attempts
Read the goal's history: 412 recorded attempts, and 212 descents dead at the class-number hypothesis, attested as an obstruction.
3 · try, record_transition
Reproduce the wall once. The failure is recorded, which keeps the obstruction's evidence current.
4 · pivot, publish
Prove what is provable today, the witness 37 ∣ numerator B₃₂, and deposit it. The theorem stays open; the store is one verified entry richer.
Simulated replay: payload shapes are the live API's; obstruction-grade retrieval arrives with the identity benchmark and janitor stages.
On hard problems the cache's first value is negative: knowing that 212 descents already died at the class-number wall, before spending anything. Its second value compounds: the published witness shortens every future attempt in this region, and the recorded failure keeps the obstruction's evidence current. How records are stored, ranked, and aged is covered in How it works.