Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
For every real $\xi>0$ the sequence of integer parts $[\xi 7^{n}]$, $n=0,1,2,\dots$, contains infinitely many composite numbers. Second, there is no infinite right truncatable prime in base~$7$.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
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.
Provider: Anthropic · Prompt public: unknown · Independence: unknown
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.
Correctness: supported · statement fidelity: unaudited · peer review: none
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Source-reported tools: computation.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.