Pith Number

pith:A6OWPH33

pith:2023:A6OWPH33AFECOYDH2KW6M5JFQI

not attested not anchored not stored refs pending

LEGO-Prover: Neural Theorem Proving with Growing Libraries

Chuanyang Zheng, Enze Xie, Haiming Wang, Han Shi, Heng Liao, Huajian Xin, Jian Yin, Jing Xiong, Lin Li, Qingxing Cao, Xiaodan Liang, Yinya Huang, Zhenguo Li, Zhengying Liu

arxiv:2310.00656 v3 · 2023-10-01 · 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{A6OWPH33AFECOYDH2KW6M5JFQI}

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.

Cited by

9 papers in Pith

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language

IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

Formalizing Mathematics at Scale

Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin

Receipt and verification

First computed	2026-07-05T07:05:47.926377Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

079d679f7b0148276067d2ade675258205bb0cbd26b2a4de7bf04a87bc2c2282

Aliases

arxiv: 2310.00656 · arxiv_version: 2310.00656v3 · doi: 10.48550/arxiv.2310.00656 · pith_short_12: A6OWPH33AFEC · pith_short_16: A6OWPH33AFECOYDH · pith_short_8: A6OWPH33

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/A6OWPH33AFECOYDH2KW6M5JFQI \
  | 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: 079d679f7b0148276067d2ade675258205bb0cbd26b2a4de7bf04a87bc2c2282

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "626f7a7ec5f3c6931ae27c1c0675ce33cec608690a8e044a7fea50f709ff790c",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.AI",
    "submitted_at": "2023-10-01T12:47:59Z",
    "title_canon_sha256": "ad81f56158a93a7a0d48d083c1f08c7035d9fd34f49637f277a1b8a220fec4df"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2310.00656",
    "kind": "arxiv",
    "version": 3
  }
}