Reciprocal Fermat Constant is Nonnormal
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Theory of Normal Numbers and Digit Expansions
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-09-08
- Model
- ChatGPT-6 Astra
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 18 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The paper proves that the reciprocal Fermat constant is disjunctive but nonnormal in binary, explicitly locates every finite word, and establishes positive lower word frequencies. It extends these properties to a broad family of arithmetic series. Behavior in unrelated bases remains open.
What the AI did
Astra developed several techniques in a previous work we did together. I asked it to find problems where the techniques could be of use, it chose the constant, proved it was disjunctive in base 2, proved it was nonnormal in base 2, then generalized the result.
Verification
Full Lean verification is here: https://github.com/CaptainSude/reciprocal-Fermat-constant-Nonnormal/releases/tag/v1.0.0
Source
- Lean proofGitHub repository with Lean proof
Submitted by nufrogcaca on