Pith Number

pith:S2HQQEKU

pith:2026:S2HQQEKU7DMBQORWYNSKSNVWQU

not attested not anchored not stored refs resolved

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Clark Barrett, Elizaveta Pertseva, James Parker, Valentin Robert

Lean tactic automates finite field to bitvector translations and solves 19% more ZKP benchmarks than SMT solvers

arxiv:2605.15163 v1 · 2026-05-14 · cs.LO

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

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{S2HQQEKU7DMBQORWYNSKSNVWQU}

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 approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

C2weakest assumption

That the range lemmas and case analysis in BitModEq produce sound translations for all relevant cases in ZKP arithmetization without missing edge cases or introducing incorrect equivalences.

C3one line summary

A new Lean tactic automates bitvector-finite field equivalence proofs and solves 19% more ZKP arithmetization benchmarks than state-of-the-art SMT solvers.

References

45 extracted · 45 resolved · 0 Pith anchors

[1] Isa semantics for armv8-a, risc-v, and cheri-mips.Proceedings of the ACM on Programming Languages, 3(POPL): 1–31, 2019 2019

[2] Jolt: Snarks for virtual machines via lookups 2024

[3] A verified algebraic representation of cairo program execution 2022

[4] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reyn 2022

[5] Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kre- mer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Math- ias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zoha 2023 · doi:10.1145/3587692

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-17T21:40:25.356670Z
Last reissued	2026-05-17T21:57:18.679818Z
Builder	pith-number-builder-2026-05-17-v1
Signature	unsigned_v0
Schema	pith-number/v1.0

Canonical hash

968f081154f8d8183a36c364a936b68518e25c720a5e5b942e02c6583433d1fb

Aliases

arxiv: 2605.15163 · arxiv_version: 2605.15163v1 · pith_short_12: S2HQQEKU7DMB · pith_short_16: S2HQQEKU7DMBQORW · pith_short_8: S2HQQEKU

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/S2HQQEKU7DMBQORWYNSKSNVWQU \
  | 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: 968f081154f8d8183a36c364a936b68518e25c720a5e5b942e02c6583433d1fb

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "42b36ed7b516c8f43b2130c86e1a69fa96523ff20be8182cad1ffadab506fb52",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-14T17:54:04Z",
    "title_canon_sha256": "de3128f6dcc9910d16319df8b827aeae8700a2a4980dff811cbb5a1b214c0d7f"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15163",
    "kind": "arxiv",
    "version": 1
  }
}