Pith Number

pith:SJ5FT4V2

pith:2026:SJ5FT4V2QHUVZ5YACI35Q3D5GY

not attested not anchored not stored refs resolved

LeanBET: Formally-verified surface area calculations in Lean

Colin T. Jones, Ejike D. Ugwuanyi, John Velkey, Tyler R. Josephson

A fully executable BET surface area pipeline has been formally verified in Lean with proofs over the reals and floating-point execution that matches a reference implementation.

arxiv:2605.16169 v1 · 2026-05-15 · cs.LO · cs.MS · physics.chem-ph

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

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{SJ5FT4V2QHUVZ5YACI35Q3D5GY}

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

We show that the regression coefficients returned by the algorithm agree with their specification-level definitions and minimize the least-squares error under the stated assumptions. We also prove that the window enumeration is sound and complete, and that the admissibility checks and knee-based selection satisfy their formal specifications.

C2weakest assumption

The floating-point implementation is assumed to be a faithful enough approximation of the real-number proofs for the numerical results to be trusted in practice; the paper does not supply a formal proof of the floating-point semantics themselves.

C3one line summary

LeanBET supplies a fully executable, formally verified BET analysis pipeline in Lean 4 whose regression coefficients and window selections match their real-number specifications and agree with the BETSI reference to machine precision on 18 of 19 isotherms.

References

21 extracted · 21 resolved · 1 Pith anchors

[1] Stephen Brunauer, P. H. Emmett, and Edward Teller. Adsorption of Gases in Multimolecular Layers. Journal of the American Chemical Society, 60(2):309–319, February 1938. URL:https://pubs.a cs.org/doi/a 1938 · doi:10.1021/ja01269a023

[2] Van Erp and Johan A 2011 · doi:10.1016/j.micromeso.20

[3] Johannes W. M. Osterrieth, James Rampersad, David Madden, Nakul Rampal, Luka Skoric, Bethany Connolly, Mark D. Allendorf, Vitalie Stavila, Jonathan L. Snider, Rob Ameloot, João Marreiros, Conchi Ania, 2022 · doi:10.1002/adma.202201502

[4] Macdonald, Vladimir Martis, and Ivan P 2018 · doi:10.1002/smtd.201800173

[5] D.D. Do, H.D. Do, and D. Nicholson. A computer appraisal of BET theory, BET surface area and the calculation of surface excess for gas adsorption on a graphite surface.Chemical Engineering Science, 65 2010 · doi:10.1016/j.ces.2010.02.023

Formal links

2 machine-checked theorem links

Receipt and verification

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

Canonical hash

927a59f2ba81e95cf7001237d86c7d361886426727019f59617bca5daeb93925

Aliases

arxiv: 2605.16169 · arxiv_version: 2605.16169v1 · doi: 10.48550/arxiv.2605.16169 · pith_short_12: SJ5FT4V2QHUV · pith_short_16: SJ5FT4V2QHUVZ5YA · pith_short_8: SJ5FT4V2

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/SJ5FT4V2QHUVZ5YACI35Q3D5GY \
  | 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: 927a59f2ba81e95cf7001237d86c7d361886426727019f59617bca5daeb93925

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "f59c4cf8da4c406529c58c2086fa0d21b3925d8a5ac831c1a79c4e865c203d6a",
    "cross_cats_sorted": [
      "cs.MS",
      "physics.chem-ph"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-15T16:48:52Z",
    "title_canon_sha256": "f2115eeb4e6229c17dc88c7f32e48564775b000a4477f619c2b794f37f67a4ed"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.16169",
    "kind": "arxiv",
    "version": 1
  }
}