Five `research solved` declarations depend on `native_decide` axioms

`PROOFS.md` scopes `native_decide` to test declarations —

> For a large computation in a `category test` declaration, `native_decide` may be acceptable.
> Review this case by case.

— and asks that native-evaluation axioms be reported:

> Native evaluation can add axioms such as `Lean.ofReduceBool` or `Lean.trustCompiler`; report
> them when they are relevant.

Five `research solved` declarations currently depend on such axioms. I ran `#print axioms` on each
against `main` (`2a0126f6`); the output is below verbatim.

Most `native_decide` use in the repository is fine — of 444 occurrences across 101 files, the large
majority sit in `category test` value computations, exactly as `PROOFS.md` allows. These five are
the ones that land on a `research` declaration.

---

- [ ] [`selfridge_78557`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Wikipedia/SierpinskiNumber.lean#L51-L53) — **8** native axioms

```
'SierpinskiNumber.selfridge_78557' depends on axioms: [propext, Classical.choice, Quot.sound,
SierpinskiNumber.selfridge_78557._native.native_decide.ax_1_1, … ax_1_8]
```

- [ ] [`erdos_394.variants.factorial_gap_10`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/394.lean#L129-L131) — **6** native axioms

- [ ] [`erdos_686.variants.non_square`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/686.lean#L125-L127) — **2** native axioms

- [ ] [`erdos_340.variants._22_mem_sub`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/ErdosProblems/340.lean#L118-L120) — **1** native axiom

- [ ] [`selfridge_seq_conjecture.variants.sufficient_condition`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Wikipedia/Selfridge.lean#L139-L141) — **1** native axiom

---

### Why this might matter

`research solved` is the repository's strongest claim about a statement, and `PROOFS.md`'s own
`formal_proof` checklist asks contributors to run `#print axioms` and check for custom axioms. A
reader applying that checklist to these five finds compiler-generated axioms rather than the
standard three, so the proofs are not kernel-checked.

### Possible responses, in increasing order of effort

1. **Document it.** Note in each docstring that the proof uses `native_decide`, so the axiom
footprint is visible without running `#print axioms`.
2. **Recategorise the computational part.** Where the native computation is a finite check, split it
into a `category test` lemma (which `PROOFS.md` sanctions) and keep the research declaration
depending on it — though that moves the axioms rather than removing them.
3. **Replace with kernel-checked proofs.** `selfridge_78557` looks the most tractable: that 78557 is
a Sierpiński number is a covering-congruence argument over a fixed finite set of primes, which
should be provable by `decide`/`norm_num` on each congruence class rather than by native
evaluation. I have not attempted it.

I am not proposing a change here — this is a report, and the right threshold is the maintainers' to
set. Happy to attempt (3) for `selfridge_78557` if that would be useful.

### Not a finding

`erdos_387.variants.schinzel` also contains `native_decide`, but it is `research open` with an
`answer(sorry)` statement, so its `sorryAx` dependence is expected and it is excluded above.

*AI assistance: found and verified with Claude Opus 5 — the scan, the `#print axioms` runs against
`main`, and the category checks are mine.*

Read PROOFS.md and inspect the five linked declarations in SierpinskiNumber.lean, ErdosProblems/394.lean, ErdosProblems/686.lean, ErdosProblems/340.lean, and Selfridge.lean. Re-run #print axioms against the relevant revision, then confirm the maintainers' chosen response and verify that all five declarations meet it.

Written by the indexing model from the issue text.