# AlphaProof Nexus OEIS Reconciliation — 2026-07-20

Status: `UNRECONCILED AUTHOR CLAIM`

## Question and counting unit

The AlphaProof Nexus paper reports 44 successful conjectures among 492
autoformalized OEIS questions. The denominator is a set of 492 attempted Lean
theorem records, so the first reconciliation unit is the attempted target
theorem, not the number of OEIS pages, helper lemmas or informal statements
described on an OEIS page.

This audit asks whether 44 successful attempted theorem records can be
identified in the official public material.

## Sources inspected

- AlphaProof Nexus arXiv v1 and v2, including the v2 TeX source and supplement;
- the complete `main` history, branches, tags and releases of the official
  AlphaProof Nexus results repository;
- the pinned 492-row `THEOREM_MAPPING.txt` from the Formal Conjectures
  `auto_oeis` branch;
- all Lean files under `APNOutputs/OEIS` at result commit
  `0647711a71183c1ea492ad60860776617ce1ea88`;
- public issue 1 in the results repository.

The exact artifact-to-attempt join is preserved in
`data/alphaproof_nexus_oeis_theorem_mapping.csv`.

## Reproduced results

| Test | Result |
|---|---:|
| attempted theorem-mapping records | 492 |
| public OEIS Lean result files | 38 |
| exact result-stem matches in the 492-row mapping | 38 |
| target theorem declarations across those files | 38 |
| public result files with other than one target theorem | 0 |
| unique OEIS sequence IDs represented | 37 |
| successful attempted records not represented publicly, if 44 is the unit | 6 |

A248802 has two distinct public result files and therefore explains why 38
attempted theorem records correspond to 37 OEIS sequence IDs. It does not
close the six-record gap.

## Repository-history check

The official repository has six commits on one public branch and no public
tags or releases. The first two commits contain 39 files in the OEIS output
directory. One of them is `GraphConjecture2.lean`, a graph-theory result placed
in the wrong directory. Commit `77378c192ed3f865fe3947829462fedea3f1d099`
moves that file out of OEIS, leaving the same 38 in-scope OEIS result files
present at the current revision.

No public revision inspected contains 44 in-scope OEIS result artifacts.

## Paper-supplement check

Both paper versions retain the 44/492 statement. The v2 source includes two
OEIS supplementary proofs, A051293 and A228143, and points to the public result
directory for their Lean files. It does not include a table or list identifying
all 44 successes.

Some OEIS pages describe multiple informal conjectures or consequences around
one result. That cannot be used to manufacture the missing six here: each
public result maps to one of the 492 attempted theorem records and contains one
target theorem declaration. Counting helper results or informal consequences
would silently change the numerator's unit while leaving the denominator in
attempted-theorem units.

## Public issue check

Issue 1, titled `OEIS proofs`, raised the same discrepancy on 24 May 2026 and
asked for the remaining natural-language and Lean proofs. The requester closed
it later that day. The public thread contains no reply, linked commit or
explanation.

## Conclusion

The denominator is reconstructed. The public numerator is reconstructed only
to 38 successful attempted theorem records representing 37 OEIS sequences.
The official public repository, its history, the paper supplement and the
public issue thread do not identify the other six records or provide a counting
rule that produces 44 from the public artifacts.

This does **not** establish that 44 is false. It establishes that 44 is not
independently reconstructable from the inspected public evidence. The workpack
must therefore retain it as an `author_claim_unreconciled`, not promote it to a
verified event count, and not infer six missing results.

## Publication-safe wording

> The paper reports 44 successes among 492 attempted OEIS conjectures. In the
> pinned public result repository, Hedegreen Research could reconstruct 38
> successful attempted theorem records representing 37 OEIS sequences. The
> remaining six were not identified in the public repository, its history, the
> paper supplement, or the public issue thread.

## Exact next evidence request

Ask the corresponding authors or repository maintainers for either:

1. the six additional theorem names and public artifacts; or
2. the counting rule that maps the released artifacts to 44 successful members
   of the 492-row attempted cohort.

Until one of those is supplied, the discrepancy is documented rather than
closed.