Pith Number

pith:HYDIVZQ5

pith:2026:HYDIVZQ5TZCPPT2PQIZ2NLGXQG

not attested not anchored not stored refs resolved

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Gaolei He, Hanrui Zhao, Jianlin Wang, Ruobing Zuo, Zhengfeng Yang

LLM-suggested approximate sum-of-squares decompositions can be refined symbolically into exact Lean-verified proofs for polynomial inequalities with up to 10 variables.

arxiv:2605.15445 v1 · 2026-05-14 · cs.AI

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{HYDIVZQ5TZCPPT2PQIZ2NLGXQG}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

NSPI provides an end-to-end pipeline from LLM heuristic discovery to machine-checked proof for polynomial inequalities and demonstrates effectiveness and scalability on challenging benchmarks involving polynomials with up to 10 variables.

C2weakest assumption

The assumption that LLM-generated approximate SOS decompositions are sufficiently close to exact ones that symbolic refinement can always (or mostly) succeed without prohibitive cost or failure on the target benchmarks.

C3one line summary

NSPI uses LLMs to generate approximate SOS conjectures for polynomial inequalities, refines them symbolically into exact proofs, and certifies them in Lean, scaling to benchmarks with up to 10 variables.

References

15 extracted · 15 resolved · 0 Pith anchors

[1] 9 From LLM Conjectures to Lean Formalizations: Automated Inequality Proving via Sum-of-Squares Certificates Heule, M 1993 · doi:10.1016/j.jsc.2011.08.002

[2] URL https://www.sciencedirect.com/ science/article/pii/S0304397508006452 2008 · doi:10.1016/j.tcs.2008.09.025

[3] The polynomialf(x)admits a rational SOS decomposition, that is, there exist polynomialsf i(x)∈Q[x]such that f(x) = rX i=1 fi(x)2

[4] There exists a symmetric positive semidefinite Gram matrixG∈S m ∩Q m×m such that f(x) =v(x) ⊤Gv(x), G⪰0. For the numerical solution GN obtained after the Gauss–Newton refinement, when the backward err 2013

[5] Analyze the input polynomial carefully, focusing on the coefficients and the combinations of variables involved

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-20T00:00:59.003815Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

3e068ae61d9e44f7cf4f8233a6acd781910f09631b54b15bf1b413786c80d631

Aliases

arxiv: 2605.15445 · arxiv_version: 2605.15445v1 · doi: 10.48550/arxiv.2605.15445 · pith_short_12: HYDIVZQ5TZCP · pith_short_16: HYDIVZQ5TZCPPT2P · pith_short_8: HYDIVZQ5

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/HYDIVZQ5TZCPPT2PQIZ2NLGXQG \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 3e068ae61d9e44f7cf4f8233a6acd781910f09631b54b15bf1b413786c80d631

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "ea69fe50e793b3e011f79a0a1ffd0754bbb91b7617ef70cc7564d990d0c9662a",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.AI",
    "submitted_at": "2026-05-14T22:02:31Z",
    "title_canon_sha256": "70a1b5636a2a737368fd27bec08a773a4491abeb571377f0bd7ef5658b205527"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15445",
    "kind": "arxiv",
    "version": 1
  }
}