Composites Among and Right-Truncatable Primes in Base 7
For every real the sequence of integer parts , , contains infinitely many composite numbers. Second, there is no infinite right truncatable prime in base~.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Number theory - integer sequences
- Posed by
- Forman and Shapiro (1967), Dubickas and Novikas (2005)
- Year posed
- 2005
- Years open
- 21y
- Solved
- 2026-08-15
- Model
- Fable 5, Opus 4.8
- Vendor
- —
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
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 by this site on 17 August 2026. The entry arrived titled with a person's name and claiming Lean-verified; both needed correcting. The submitter's own note says the Lean check rests on a massive native_decide certificate check - native_decide bypasses the kernel through the compiled evaluator, which is precisely the distinction this site's tier ladder exists to record - and, more fundamentally, no public Lean repository is linked anywhere on the entry: the only artifact is a ResearchGate manuscript. A formalization that cannot be fetched cannot hold any Lean tier, so this sits at Unreviewed. If the Lean development is published (with its native_decide dependence stated), the tier can move to Lean-checked on a source audit.
Source
Submitted by LucidKestrel185 on