Pith Number

pith:CK77J6CV

pith:2026:CK77J6CVPFWHZU4WIC6Z6NTXIZ

not attested not anchored not stored refs resolved

A Minimal Agent for Automated Theorem Proving

Austin Letson, Borja Requena, Izan Beltran-Ferreiro, Krystian Nowakowski, Leopoldo Sarra

A minimal agent achieves competitive theorem proving performance with iterative refinement, library search, and context management at a fraction of state-of-the-art costs.

arxiv:2602.24273 v3 · 2026-02-27 · 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{CK77J6CVPFWHZU4WIC6Z6NTXIZ}

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

Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture and a fraction of their cost.

C2weakest assumption

The assumption that the implemented core features (iterative refinement, library search, context management) are sufficient to achieve competitive results across qualitatively different benchmarks without additional specialized components.

C3one line summary

A minimal agentic system achieves competitive performance in automated theorem proving with a simpler design and lower cost than state-of-the-art methods.

References

87 extracted · 87 resolved · 9 Pith anchors

[1] Davis, Guillaume Baudart, and Louis Mandel 2021 · doi:10.1007/978-3-030-

[2] Lars Becker et al.A blueprint for the formalization of Carleson’s theorem on convergence of Fourier series. 2025. arXiv:2405.06423 [math.CA] .url: https://arxiv.org/abs/ 2405.06423 2025

[3] Ben Cottier, Ben Snodin, David Owen, and Tom Adamczewski 2023

[4] Olympiad-level formal mathematical reasoning with reinforcement learning.Nature 2025 · doi:10.1038/s41586-025-09833-y

[5] Aristotle: IMO-level Automated Theorem Proving 2025 · arXiv:2510.01346

Receipt and verification

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

Canonical hash

12bff4f855796c7cd39640bd9f367746740a481eda51a50f6c8e92284971e060

Aliases

arxiv: 2602.24273 · arxiv_version: 2602.24273v3 · doi: 10.48550/arxiv.2602.24273 · pith_short_12: CK77J6CVPFWH · pith_short_16: CK77J6CVPFWHZU4W · pith_short_8: CK77J6CV

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/CK77J6CVPFWHZU4WIC6Z6NTXIZ \
  | 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: 12bff4f855796c7cd39640bd9f367746740a481eda51a50f6c8e92284971e060

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "7876b58733134eda9a645d6306e3207c9a5b992acd3012f746c1bfa68f6d9dbe",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.AI",
    "submitted_at": "2026-02-27T18:43:47Z",
    "title_canon_sha256": "4138a86950985f0b6156a71c8745ff86b466186134f13555f49ea92369a7906b"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2602.24273",
    "kind": "arxiv",
    "version": 3
  }
}