One-sentence Summary

Using the MechMath Agent Team to generate both the natural-language proof and its Lean 4 formalization, this paper proves that every nonnegative integer is the sum of a triangular, pentagonal, and heptagonal number, thereby settling the OEIS A287616 conjecture.

Key Contributions

• The paper proves that every nonnegative integer can be expressed as x(x+1)/2 + y(3y+1)/2 + z(5z+1)/2 for natural numbers x, y, and z, thereby resolving the OEIS A287616 conjecture.
• The MechMath Agent Team framework automatically generates both the natural-language proof and the corresponding Lean 4 formalization for this result.
• The resulting Lean 4 formalization covers the complete derivation, with only an externally cited theorem and a symbolic computation verification remaining unformalized.

Introduction

Number theory has long investigated how integers decompose into sums of specialized sequences like polygonal numbers, a foundational pursuit that strengthens additive combinatorics and informs algorithmic approaches to integer representation. Earlier work successfully proved that every nonnegative integer is a sum of three triangular numbers, yet extending these results to mixed polygonal families demanded cumbersome case analysis and left many combinations unverified. The authors leverage systematic algebraic reduction and targeted computational verification to demonstrate that every nonnegative integer can be expressed as the sum of exactly one triangular, one pentagonal, and one heptagonal number. This contribution resolves a targeted gap in the generalized polygonal number theorem and establishes a clear pathway for future additive investigations.

Dataset

• Dataset composition and sources: The authors provide a publicly accessible repository that serves as the complete data archive for the project. It contains the full Lean 4 source code, build instructions, and exact computer certificates generated for a finite cover proof.
• Subset breakdown: The repository is organized into two distinct packages. The formalization/ package contains the Lean development files and is built against Mathlib v4.29.0. The verification/ package holds the exact two-tier cover structure, individual per-unit certificates, and a standalone verifier.
• Usage and organization: The authors use the repository to ensure complete reproducibility and transparency. A detailed README maps each ingredient of the mathematical proof directly to its corresponding Lean formalization or certificate artifact, creating a clear reference trail for readers.
• Processing and verification details: The project relies on a Lake project structure for dependency management and formal development. The verification workflow utilizes a custom verifier that processes the per-unit certificates to independently re-derive the proof verdicts, guaranteeing that every mathematical step is backed by machine-checkable evidence.

Method

The authors leverage a reduction strategy that transforms the original representation problem into a constrained ternary quadratic form problem. By applying elementary square identities, the target equation is mapped to $Q(u, v, w) = 15u^2 + 5v^2 + 3w^2$Q(u,v,w)=15u2+5v2+3w2, where the objective is to find integer coordinates satisfying specific parity and congruence conditions. This transformation shifts the computational focus to constructing a primitive representation and systematically improving it through a structured descent process.

The framework begins by establishing a primitive seed for any valid input. The authors employ $p$p-adic Hensel lifting to verify local representability across all prime moduli. They then apply a genus-theoretic local-global principle, which guarantees that the quadratic form or its genus mate primitively represents the target integer. A rational transfer mechanism bridges the genus mate representation back to the original form, ensuring a valid primitive starting point for the subsequent descent phase.

Once a primitive representation is obtained, the authors implement a finite descent procedure guided by a lexicographic potential function. The descent relies on a set of rational similarity transformations that preserve the quadratic form and maintain coordinate primitivity. Each transformation is designed to strictly decrease the potential function by adjusting coordinate parities and residue classes. The authors define five elementary one-step descent rules that cover the majority of the search space, routing states toward the target congruence conditions through sign lifts and modular adjustments.

The elementary descent rules leave a narrow residual region where standard moves cannot immediately satisfy the required conditions. To resolve this gap, the authors partition the residual space into a finite number of sign-residue cells. They prove that the success of any short descent word depends only on a bounded set of sign evaluations and modular residues. This determinacy property reduces the infinite descent problem to a finite verification task. The authors then construct an exact rational linear programming cover that enumerates all realizable subcells within the residual cone. Each subcell is certified with an explicit integer witness and a bounded-length escape word, guaranteeing that the descent terminates at a valid state without relying on floating-point arithmetic or sampling.

The entire mathematical core is encoded in a proof assistant framework. The authors formalize the square reduction, the primitive seed construction, the transport identities, the elementary descent calculus, and the residual gap analysis. The formalization isolates two external inputs: a classical genus local-global theorem and the finite linear programming cover certificate. All logical dependencies are kernel-checked, ensuring that the descent algorithm and the final representation theorem are machine-verified.

Experiment

The experiment evaluates a two-tier covering strategy for sign cones intersecting a residual cone, validating whether algebraic words of varying lengths can effectively certify sign behavior across different geometric regions. Analysis reveals that nearly all cones are successfully verified using depth-three words, while a small subset of ceiling cones requires length-four words and explicit geometric verification of extreme rays. This tiered approach efficiently bounds sign variation for new forms, demonstrating that combining targeted word lengths with precise rational cone checks reliably captures sign changes throughout the arrangement.

The authors present a computational analysis of a two-tier cover, noting that most sign cones are resolved with depth-three words while a small number require length-four words. The experiment quantifies the complexity of this verification, showing that the process generates a significantly larger volume of closer pullback emissions compared to exact row states. The extended arrangement is shown to include a substantial number of new forms relative to the original set. The volume of closer pullback emissions greatly exceeds the count of exact row states. The set of new forms constitutes a major portion of the total forms in the union. The experiment differentiates between distinct coordinate-read forms and pulled-back closer forms.

The authors analyze a two-tier cover structure involving sign cones and ceiling cones, noting that the majority of cones are simple while a small subset requires complex certificates. The experiment quantifies the structural complexity by tracking exact row states, emissions, and various forms. The results indicate that closer pullback emissions significantly outnumber exact row states, and pulled-back closer forms are more numerous than coordinate-read forms. The analysis distinguishes between simple sign cones and complex ceiling cones, with the latter requiring exact rational cone membership checks. The data shows a significantly larger volume of closer pullback emissions compared to exact row states. The count of distinct pulled-back closer forms is notably higher than the count of distinct coordinate-read forms.

The computational analysis evaluates a two-tier cover structure to assess the verification complexity and structural expansion of sign and ceiling cones. The experiment demonstrates that while most cones are structurally simple and resolve with minimal depth, a small subset requires more intricate rational membership checks. Qualitatively, the verification process yields a substantially larger volume of closer pullback emissions and pulled-back forms compared to exact row states and coordinate-read forms, indicating that extended arrangements significantly broaden the overall form space.