A neutral schematic of the objects and relations in the statement.
Problem. An addition chain starts at \(1\) and appends sums of two earlier terms. What is the minimum length \(\ell(2^{127}-1)\) of an addition chain ending at \(2^{127}-1\)?
1Context
Current rigorous bounds are 127 <= ell(2^127-1) <= 136. The gap is small enough for defect-based enumeration while the endpoint is far beyond direct integer-state BFS.
2Problem setup
Definition 1. The length is the number of appended terms, so the initial 1 has length zero.
Remark 1. Repeated summands are allowed.
3What counts as a solution
Give a shortest chain and a certificate excluding every shorter length.
1Status
Current status (The strongest located interval is 133 through 136). A reported exhaustive Hamming-weight result gives the lower endpoint, while an explicit 136-step addition chain gives the upper endpoint.[1]
1Records
5 records
Record
Kind
Assessment
Result
Supported
claim · Proposition 1
A reported exhaustive Hamming-weight result gives the lower endpoint, while an explicit 136-step addition chain gives the upper endpoint.[1]
Relevance to this problem
For Shortest addition chain for the 127th Mersenne number, record m127ac-claim-current-bounds (“The strongest located interval is 133 through 136”) records a bound, answer, status fact, or structural consequence. The record states: A reported exhaustive Hamming-weight result gives the lower endpoint, while an explicit 136-step addition chain gives the upper endpoint.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Put
\[
N=2^{127}-1=170141183460469231731687303715884105727.
\]
The strongest bound located in the literature and database audit is
\[
133\leq \ell(N)\leq136.
\]
The upper endpoint is independently replayed in this dataset. The lower endpoint uses Neill Clift's exhaustive verification of the Knuth-Stolarsky inequality for every integer of binary Hamming weight at most 128, as reported in Achim Flammenkamp's addition-chain database. Since
\[
\lambda(N)=\lfloor\log_2N\rfloor=126,
\qquad \nu(N)=127,
\]
that result gives
\[
\ell(N)\geq126+\lceil\log_2 127\rceil=133.
\]
The public report states the scope and completion date, November 2023, but the audit did not locate a compact certificate that can be replayed inside this fixture. For comparison, the published analytic theorem of Schönhage independently gives \(\ell(N)\geq132\).
No source found in the audit proves that 136 is optimal or supplies a chain of length at most 135. The four possible values 133, 134, 135, and 136 therefore remain open on the evidence recorded here.
Result
Reproduced
claim · Computation 1
Brauer's star-chain construction expands a ten-step chain for 127 into a checked 136-step chain for 2^127-1.[2]
Relevance to this problem
For Shortest addition chain for the 127th Mersenne number, record m127ac-claim-brauer-upper (“An explicit addition chain reaches the target in 136 steps”) records a bound, answer, status fact, or structural consequence. The record states: Brauer's star-chain construction expands a ten-step chain for 127 into a checked 136-step chain for 2^127-1.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
established
Scope
the target N=2^127-1 and the exponent star chain (1,2,3,5,7,14,28,56,63,126,127)
For \(M_r=2^r-1\), use the star chain
\[
1,2,3,5,7,14,28,56,63,126,127.
\]
Each new exponent has the form \(a+b\), where \(a\) is the preceding exponent and \(b\) already occurs. Starting with \(M_a\), perform \(b\) doublings and then add the earlier value \(M_b\). The identity
\[
2^bM_a+M_b=M_{a+b}
\]
shows that this reaches the next Mersenne value.
The exponent increments sum to \(127-1=126\). There is one final addition for each of the ten star steps, so the expanded chain has length
\[
126+10=136.
\]
The complete 137-value chain is stored in `m127ac-artifact-chain-replay`. Its final three values are
\[
2^{126}-2,\quad 2^{127}-2,\quad 2^{127}-1.
\]
The artifact checks every predecessor pair and the final target.
Settling the target requires either a chain of length at most 135 or a certificate excluding all three shorter lengths.[4]
Relevance to this problem
For Shortest addition chain for the 127th Mersenne number, record m127ac-open-three-step-gap (“Three shorter lengths remain unresolved”) records a bound, answer, status fact, or structural consequence. The record states: Settling the target requires either a chain of length at most 135 or a certificate excluding all three shorter lengths.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
open
Scope
exclusion or construction of addition chains of lengths 133, 134, and 135 for N=2^127-1
The 136-step construction does not prove optimality. The lower-bound audit excludes lengths through 132 according to the reported exhaustive Hamming-weight result. It leaves lengths 133, 134, and 135.
A complete solution can take either form: an explicit shorter chain, or an exhaustive certificate ruling out each remaining length. Any future lower-bound computation should publish enough reduced-graph, defect-pattern, or search-frontier data for independent replay.
Schönhage's theorem is an independently checkable floor, while Clift's reported Hamming-weight sweep raises it by one.[3][1][2][5][4]
Relevance to this problem
For Shortest addition chain for the 127th Mersenne number, record m127ac-attempt-lower-bound-audit (“Published theory gives 132; the current enumeration report gives 133”) documents a concrete method, search boundary, or failed route. The record states: Schönhage's theorem is an independently checkable floor, while Clift's reported Hamming-weight sweep raises it by one.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
completed
Scope
lower bounds for the ordinary addition-chain length of N=2^127-1
Schönhage proved
\[
\ell(n)\geq\log_2 n+\log_2\nu(n)-2.13,
\]
where \(\nu(n)\) is the number of ones in the binary expansion. Substitution of \(N=2^{127}-1\) and \(\nu(N)=127\) gives a right side of approximately \(131.8586846868\). Since chain length is integral,
\[
\ell(N)\geq132.
\]
This is the strongest lower endpoint reproduced here solely from a peer-reviewed universal theorem.
The Knuth-Stolarsky inequality asserts
\[
\ell(n)\geq\lambda(n)+\lceil\log_2\nu(n)\rceil.
\]
Flammenkamp's maintained database reports that Neill Clift completed an exhaustive verification for every target with \(\nu(n)\leq128\) in November 2023. Applying the reported result to the present target gives 133. The same page distinguishes this finite verified range from the unresolved universal conjecture.
Brauer's 1939 paper supplies the star-chain construction behind the upper endpoint. Clift's 2011 paper gives an exact-search framework for point values, and the current additionchains.com site documents ongoing computations. The audit found no peer-reviewed or database entry settling \(\ell(2^{127}-1)\), and no shorter explicit chain than the 136-step construction recorded here.
A standard-library verifier reconstructs the displayed chain, checks all 136 sums, and fixes its canonical digest.
Relevance to this problem
For Shortest addition chain for the 127th Mersenne number, record m127ac-artifact-chain-replay (“Replayable 136-step addition chain”) supplies evidence or a replay used to check the packet. The record states: A standard-library verifier reconstructs the displayed chain, checks all 136 sums, and fixes its canonical digest.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
available
Scope
all 136 additions in the displayed chain ending at 2^127-1
Entry point
join source_lines with newline and run with python3
Runtime
CPython 3, standard library only
Details
The `chain_values_decimal` field is the complete chain in order, including the initial 1. The verifier reconstructs the same list from the exponent star chain. For every appended value it records the two earlier indices used in the sum, checks those indices, checks strict increase, and verifies the final target.
The canonical compact JSON encoding of the integer list has SHA-256 digest `fb5519926465307c1ea1fd9901cbc1adbf329f51ccd0c820c3f8feef4b34f08f`. The compact report has digest `a51cd95631b6424c80e0d70e8a112814f61603489f60b02300d4763de2c03014`.
Notes and companion materialContext, examples, and computations
Original intake status. UNKNOWN as of 2026-07-28. A replayed chain gives ℓ(2^127−1)≤136, and current lower-bound tables leave a finite gap. No checked source determines the exact shortest length.
The 2026-07-28 exact-integer search found no certified optimum for 2^127−1.
The packet contains a replayable 136-step upper certificate and a separately sourced lower endpoint.
No duplicate exact Mersenne-127 target was found in the controlled corpus.
Recorded example 1. The lower bound 127 follows because a chain of length 126 reaches at most 2^126.
Computational notes
The displayed 10-step star chain for exponent 127 was checked term by term. Expanding each star step with M_(a+b)=2^b M_a+M_b gives a recoverable addition chain of length (127-1)+10=136 for the target.
How the 5 records connectTyped relations and evidence flowHow the records connect to the problem
ProblemShortest addition chain for the 127th Mersenne number
TheoremDB contributors, “Shortest addition chain for the 127th Mersenne number,” TheoremDB research memory, snapshot of July 25, 2026. https://theoremdb.org/statements/mersenne-127-addition-chain
This problem includes 5 records joined by 4 typed links, sourced from wwwhomes.uni-bielefeld.de[1], current as of July 25, 2026.
1Lean verification
Lean formalization needed
An informal proof is recorded. A Lean formalization still needs to be attached. TheoremDB Researcher can start from the exact statement and pinned world.
The prefilled request prepares the target and checks drafts. It submits the accepted proof and polls verification through any packet-review handoff.
1References
Packet source. Achim Flammenkamp, Shortest Addition Chains, Conjectures section, report that Neill Clift verified the Knuth-Stolarsky inequality for every n with v(n)<=128 by November 2023; upper endpoint replayed by m127ac-artifact-chain-replay. Conjectures section and current verification notes. ↗website · reference source · web version checked 2026-08-01 · checked 2026-07-25Source use: citation only.Reports the current lower-bound verification used for the interval 133 through 136 at the 127th Mersenne number.Also cited at Achim Flammenkamp, Shortest Addition Chains, Conjectures section, report that Neill Clift verified the Knuth-Stolarsky inequality for every n with v(n)<=128 by November 2023; upper endpoint replayed by m127ac-artifact-chain-replay.Also cited at Conjectures section, November 2023 Hamming-weight verification report.For Shortest addition chain for the 127th Mersenne number: Reports the current verified lower-bound framework through exponents of binary weight at most 128.Source named by the research packet.
Alfred Brauer, “On addition chains”. Bulletin of the American Mathematical Society 45(10) (1939), 736-739. DOI 10.1090/S0002-9904-1939-07068-7. Addition-chain construction and the Scholz–Brauer relation. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Provides the classical star-chain construction specialized to the packet's 136-step certificate.Also cited at Alfred Brauer, On addition chains, Bulletin of the American Mathematical Society 45(10), 1939, pages 736-739; explicit specialization and replay in this dataset.Also cited at Bulletin of the American Mathematical Society 45(10), 1939, pages 736-739.For Shortest addition chain for the 127th Mersenne number: Supplies the classical construction specialized in the packet to the 127th Mersenne number.
Arnold Schönhage, A lower bound for the length of addition chains, Theoretical Computer Science 1(1), 1975, pages 1-12; Achim Flammenkamp, Shortest Addition Chains, current Conjectures section; Neill M. Clift, Calculating optimal addition chains, Computing 91, 2011, pages 265-284. General lower bound for addition-chain length. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Gives the general addition-chain lower bound used to constrain the exact Mersenne target.Also cited at Arnold Schönhage, A lower bound for the length of addition chains, Theoretical Computer Science 1(1), 1975, pages 1-12; Achim Flammenkamp, Shortest Addition Chains, current Conjectures section; Neill M. Clift, Calculating optimal addition chains, Computing 91, 2011, pages 265-284.Also cited at Theoretical Computer Science 1(1), 1975, pages 1-12.For Shortest addition chain for the 127th Mersenne number: Schönhage's theorem is an independently checkable floor, while Clift's reported Hamming-weight sweep raises it by one.
Gap obtained by combining the current lower-bound audit with the replayed upper-bound certificate. additionchains.com checked 2026-08-01. Exact-integer and Mersenne-number tables checked 2026-07-28. ↗website · reference source · web version checked 2026-08-01 · checked 2026-07-25Source use: citation only.Provides the current independent addition-chain tables checked for the exact Mersenne target and nearby incumbents.Also cited at Gap obtained by combining the current lower-bound audit with the replayed upper-bound certificate.Also cited at Current computational project and source-code index, checked 2026-07-25.For Shortest addition chain for the 127th Mersenne number: Settling the target requires either a chain of length at most 135 or a certificate excluding all three shorter lengths.
Computing 91, 2011, pages 265-284. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Develops the optimal addition-chain computation used by the current lower-bound tables.
Fixed addition-chain optimization for a Mersenne prime, with an explicit star-chain construction and an elementary lower bound.