Composites Among $[\xi 7^n]$ and Right-Truncatable Primes in Base 7

What the AI did

After showing that a finite computation can provably resolve the problem, it wrote programs to do the computation, resulting in a checkable certificate. It then was directed to formalize all proofs and the certificate check in Lean. Finally it was directed to write a draft of the paper from the Lean.

Verification

Reviewed and corrected 17 August 2026. The first review said no public Lean repository was linked; that was wrong - it is linked in appendix A of the paper. The error is recorded here rather than quietly dropped.

Source audit of github.com/rwst/On-Composites at commit 2e49c4d, 17 files, comments stripped before counting: no sorry, admit or axiom anywhere on the proof path. The 18 sorry occurrences are all in Challenge.lean, which nothing imports - the leanprover/comparator "statement of record", which re-declares the definitions against Mathlib alone so the solution's constants, axiom profile and fresh-export kernel re-acceptance can be checked.

The tier stops at Lean-checked for a precise reason: all five comparator configs permit exactly propext, Quot.sound and Classical.choice, and the two theorems this entry claims - infinite_composites_seven and no_infiniteTruncatablePrime_seven - are in none of them, because they rest on three native_decide calls, which decide via the compiled evaluator rather than the kernel. The repository documents that quarantine itself.

Two things bound the risk: floorPow, CompositeInt and InfiniteTruncatablePrime are verbatim identical to the Mathlib-only re-declarations comparator certifies at std3 for bases 3-6, so definitional drift is ruled out; and cond.c, cycles.c and compress.py recompute the hypotheses outside Lean. Not built here - no toolchain, and the repo has no CI - so this is a source audit, not a compile.

Sources

• Lean proofLean development, data and generating programs
• OtherOn the composites among [ξ7ⁿ]