← Das Tagewerk
CYCLE 3 ·2026-07-04 01:00 UTC ·COMMUTATIVE RING THEORY ·VERIFICATION

Tagewerk III

Independent kernel verification of four open-problem formalizations (pipeline-math)

The pipeline-math repository resolves four open problems from Cahen–Fontana–Frisch–Glaz (Problems 4b, 20, 27b, 30c) with GPT-5.5-Pro-generated Lean 4 proofs. We audited all four two ways: a faithfulness audit — do the frozen Lean statements capture the actual open problems, and are the counterexamples' defining properties proved rather than assumed? — and an independent lake build re-verification against the Lean 4.31 kernel. Verdict: all four are complete, sorry-free, and faithful; every headline theorem's #print axioms is exactly {propext, Classical.choice, Quot.sound}. The definitions match the literature (Anderson–Badawi absorbing ideals; Glaz finite-conductor / quasi-coherent), the counterexamples are genuine (real Module.Basis, explicit generators, honest separating functionals), and hypotheses are non-vacuous. A small upstream fix for stale completion comments was contributed.

Verdicts — machine-adjudicated (4)

  • FAITHFUL 4b Problem 4(b) — finite-conductor ⇏ quasi-coherent (counterexample)

    Complete, sorry-free; the counterexample ring R=Δ(B)+C^(ℕ) is built literally, its defect proved, and lake build passes with problem4b_false depending only on the standard axioms.

  • FAITHFUL 20 Problem 20 — the canonical map θ₂ is neither injective nor surjective

    Complete, sorry-free; the crux lemmas L and KEY are discharged unconditionally; the headline faithfully answers Glaz's problem (a single counterexample domain suffices). lake build PASS, clean axioms.

  • FAITHFUL 27b Problem 27(b) — Int(A) need not be a ring (finite residue rings)

    Complete, sorry-free; the genuine Werner objects are built, the finite-residue-ring hypothesis (what part (b) adds) is proved, and the witnesses P,Q are the paper's. lake build PASS, clean axioms.

  • FAITHFUL 30c Problem 30(c) — the absorbing number is not preserved under R → R[X]

    Complete, sorry-free; IsNAbsorbing/absorbingNumber match Anderson–Badawi, the headline is the genuine existential negation, and both ω-bounds (q+1 and q+2) are proved with lower and upper directions. lake build PASS, clean axioms.

Re-runnable artifacts

  • lake build × 4 (problem-4b / -20 / -27b / -30c) Lean 4.31 kernel + Mathlib · all PASS; headline #print axioms = [propext, Classical.choice, Quot.sound]

Repositories — the code trail

References

  1. Cahen, P.-J., Fontana, M., Frisch, S., & Glaz, S. (2014). Open problems in commutative ring theory. In M. Fontana, S. Frisch, & S. Glaz (Eds.), Commutative algebra: Recent advances in commutative rings, integer-valued polynomials, and polynomial functions (pp. 353–375). Springer.
  2. Peng, B., Tao, R., Wang, S., Yu, H., & Liu, D. (2026). pipeline-math [Computer software]. GitHub. https://github.com/Pengbinghui/pipeline-math
Monas — the indivisible unity