r/LLMmathematics Monthly Conjectures: Corrections, Sharp Results, and Exact Verification

Abstract

This maintained working-paper series is the citable companion to u/dForga's r/LLMmathematics post Monthly conjectures 1 (Start?), published on 25 July 2026, and to the monthly conjecture discussions that follow it. It collects precise problem statements, corrections, proofs, partial results, and exact verification artifacts. The five-page front reader now contains only open problems: centered maximal variation, the sharp Gaussian logarithmic-Sobolev stability constant, and the general conformal-factor holomorphic-embedding classification. Closed results are separated into plainly named standalone papers. For the discrete centered Hardy-Littlewood maximal operator, the record proves Var(Mf) at most Var(f) for every nonnegative sequence supported on three consecutive sites. The proof includes the complete unimodal radius-surgery argument. In the nonunimodal case, 0 at most b less than a at most c, the exact positive-variation deficit is the minimum of a-b and (a+c-2b)/3, and is strictly positive. Exact linear-real-arithmetic certificates establish the inequality for arbitrary nonnegative real profiles on at most ten consecutive sites. All seven SMT-LIB queries, complete Z3 4.16.0 proof terms, replay receipts, and the Lean-checked three-site algebra accompany a standalone three-page proof. Fresh replay parses and solves every query again; the serialized Z3 proof terms have not been checked by an independent small proof kernel. This is a fixed-dimensional trusted-solver theorem, not a uniform proof, and the general conjecture remains open. The sharp circle L1 Poincare-Wirtinger stability theorem is supplied as a standalone four-page proof. It establishes the optimal coefficient 1/4 by a nested-core coarea argument. The archive includes the LaTeX source, an independent audit, the exact 4/5 versus 9/10 counterexample to the historical common-half-arc lemma, a 65,056-profile rational diagnostic, and a bounded Lean project. For Gaussian logarithmic-Sobolev stability, the exact-root coherent pair with t squared equal to log 3 has closest coherent states at plus or minus t/2. A 640-term entropy minorant and outward-rounded 768-bit Arb calculation prove q_N < 0.577215 and Q_N < 1.15443 pi in every dimension. This is a certified upper bound, not a solution of the sharp-constant problem. The complete derivation, captured Arb balls, replay instructions, and Lean companion are provided in a standalone PDF and archive. Three further closed items each have their own short paper and source package: the deterministic cycle-discrepancy theorem and almost-sure equidistribution for random monomial unitaries; the complete flat-plane classification of holomorphic isometric embeddings into C x H, while the general conformal-factor problem remains open; and a source-level audit of the 2025 GPT-5 Pro/Gemini gradient-descent episode together with the later sharp 7/(4L) theorem of Barzilai, Shamir, and Zamani. Historical records retain their original files and credits and carry in-place notices linking to this stable concept DOI. The release comprises the five-page open-problems reader, directly visible Reddit-ready Markdown and series note, six standalone mathematical PDFs, six result-specific source or verification ZIPs, complete source and verification archives, DOI lineage, manifests, and checksums. The Reddit permalink identifies the discussion; the version DOI identifies immutable release bytes; the concept DOI identifies this evolving collection. Independent checking and priority information are welcome.