Source arithmetic
Powerful numbers and their positions on the integer line; source cases, canonical normal forms, squarefree kernels, prime valuations and congruence conditions.
Projects & results E364
Can three consecutive positive integers all be powerful?
Mathematics and formal proofActive · global conjecture open
A powerful positive integer has every prime factor appearing with exponent at least two. So 8 = 23 and 9 = 32 are powerful, but 10 = 2 × 5 is not. Erdős problem 364 asks whether a run of three exists; the conjecture is that none does.
Current public result. Paper I excludes indices divisible by 17 or 41 in a shifted-square Lucas-sequence family under stated hypotheses. See the exact statement and hypotheses.
This excludes infinite families, not the full problem. Erdős problem 364 remains open.
Public partial result
The 17/41 shifted-square obstruction
Define F0(A) = 1, F1(A) = A and Fn+2(A) = 2A Fn+1(A) + Fn(A). For a nonnegative integer A congruent to 2 modulo 4 and a positive integer N divisible by 17 or 41, Paper I proves that FN(A) - 1 is not an integer square. Positive even indices are also excluded independently, for the same A. These are restrictions within the stated recurrence setting; Erdős problem 364 remains open.
The proof makes several exact descriptions of the same candidate meet, then propagates an obstruction from the fixed indices 17 and 41 to infinitely many indices. Its force comes from that structure, not from a search through ever larger integers.
The square-middle corollary assumes X ≥ 2, X congruent to 2 modulo 8, X - 1 an integer square and X2 + 1 powerful. It restricts the exact Pell exponent defined in the article's chosen quadratic order: neither 17 nor 41 divides that exponent. It does not decide all square-middle cases or require the lower neighbour to be powerful. A genuine powerful triple would need that additional condition too.
Article v1.0.0: Theorems 1.1 to 1.3 and Corollary 1.5. Self-published, 11 September 2026; not peer-reviewed. Read the application to the triple or inspect the proof coverage and source records.
Open remainder
What remains beyond the 17/41 result.
The full conjecture remains open. Surviving a necessary condition neither constructs a powerful triple nor classifies all remaining cases.
Other recurrence indices, other square-middle families and the wider three-consecutive problem remain beyond this result. Many branch-specific exclusion, reconstruction and finiteness questions remain, and they have not been assembled into a proof of the full conjecture. Reconstruction is required only where the intended conclusion needs it, not for every exclusion.
Each proposed representation has a specific job: expose arithmetic structure, derive a necessary condition, construct a family, or reduce a remaining case to a tractable problem. The required proof depends on that job. A reduction need not preserve every detail to be useful; it must preserve the implication used by the argument.
Selected reductions and exclusions are complete. E364 is the worked problem inside Erdős Basecamp, the mathematics programme in ORBIT’s Theorems direction.
Example
Two numbers, and the definition that separates them.
A single prime factor with exponent one is enough to make a number non-powerful.
Try two numbers
72 = 23 × 32
Both primes have exponent at least two. The number is powerful.
75 = 3 × 52
The prime 3 has exponent one. The number is not powerful.
Consecutive powerful pairs exist. A run of three is the question.
7
71
8
23
9
32
10
2 × 5
A finite search with no triple rules out only its checked range unless a theorem proves that every possible solution must lie there. Computation can then complete the finite remainder, or verify an exact certificate used by a wider proof.
Representations
Source arithmetic, alternative representations, proof and exclusion.
Start with the integers, choose a description that exposes useful structure, then prove the implication needed for the conclusion.
Alternative representations
Pell and coupled Pell-type equations; Lucas and Chebyshev recurrences; quartic, Mordell-type and genus-two curves; number fields, local symbols and exact finite certificates.
Proof and exclusion
Necessary conditions, sufficient constructions and equivalences; local obstructions, fixed-prime arguments and subfamily exclusions; theorem-bounded finite checks and specified Lean proofs.
Representations
The theorem required depends on the conclusion.
Integer factorisations, normal forms, equations, recurrences and curves expose different structure. E364 records the hypotheses and proved direction of each translation before using it. Information may be discarded without invalidating a reduction; what matters is the exact implication retained. Four distinctions are important:
Equivalence
Both directions of the stated condition are proved. This does not automatically mean a one-to-one correspondence between all witnesses; uniqueness or reconstruction needs its own statement.
Necessary condition
Every original solution supplies an auxiliary solution. Proving that the auxiliary problem has no solutions rules out the original. A reverse map is not needed for this conclusion.
Sufficient construction
The stated auxiliary data construct an original solution. A complete classification additionally needs proof that all original solutions are covered.
Unproved correspondence
A promising analogy, pattern or experimental map remains research material until the needed implication is proved.
Original solution auxiliary solution
No auxiliary solution no original solution
Connection to ORBIT
Related representation questions, different standards of validation.
Inside E364, a “Rosetta stone” translation is a correspondence between mathematical descriptions. ORBIT’s wider Rosetta Stone hypothesis asks whether useful principles of geometry, dynamics and constrained systems can transfer between exact mathematics and observed AI behaviour. A translation within mathematics does not by itself establish that wider connection.
E364
Prove that a representation preserves the implication needed by a mathematical argument.
CARF
Test whether a candidate representation retains information useful for prospective prediction or a specified decision, under declared experimental conditions.
These programmes share a research concern but study different objects. Different outcomes from a stochastic system do not alone prove that its representation is inadequate. A behavioural test must assess reproducible differences and uncertainty. A theorem about the integers is not a theorem about AI safety.
Two distinct ways a representation can mislead
Several source objects may map to the same represented object. That is a many-to-one map; the set of sources mapping to one target is its fibre. Separately, an auxiliary problem can admit objects outside the image of the source map. Those extra objects are not automatically solutions of the original problem. Non-injectivity and extra auxiliary solutions are different issues, and the required proof must address the relevant one.
The representation landscape
Several routes, each with a defined mathematical role.
Hypothetical powerful triple
Normal forms and arithmetic constraints
Pell-type equationsrecurrencesalgebraic curvesfinite certificates
Formal methods and geometry
Formal proofs check specified statements.
Essential definitions, implications and subfamily results are formalised in Lean. The accompanying human statements must match their formal hypotheses and conclusions. A successful build is not a substitute for checking which proposition was proved and which axioms or unproved assumptions it depends on.
The auxiliary descriptions include Pell-type Diophantine equations, Chebyshev recurrences, quartic and Mordell-type curves, and genus-two curves. Their value lies in the arguments they enable, not simply in the availability of geometric notation.
Numerical approximation and exploratory computation can guide research. A computational step contributes to a proof when its logical role and completeness or certificate-verification argument are established. Counterexamples to proposed lemmas are retained as corrections, not concealed as failed runs.
Selected reductions and subfamily results described on this page are project-reported. Paper I has a public article and source release; other project-reported reductions still require their individual records. The general conjecture remains open. Request the mathematical record.
Evidence
Selected results are proved. The global conjecture is open.
This is a scope summary. Exact statements, proof dependencies and reproduction records belong to the technical theorem inventory.
Inspect Paper I
Article, dependencies and verification records.
Self-published v1.0.0, 11 September 2026, not peer-reviewed. Lean covers the integer-Jacobi and recurrence exclusions and propagation; the human Hilbert-reciprocity, maximality and Pell arguments are not Lean-formalised. Three historical Magma inputs are unrecovered, as the release discloses.
- Public v1.0.0 article and release: exact statements, hypotheses and the human proof.
- Proof dependencies and finite certificate explanation, with the roles of human proof, computation and Lean.
- Tagged source and verification records: exact-arithmetic verifier, PARI/GP and Python replay checks, Lean sources and axiom audit; inspect the disclosed secondary-check gaps.
- Long-form illustrated guide for further reading, not an additional independent result.
Wider evidence status
This page is a project summary, not a proof or a complete theorem inventory. The technical records distinguish formal proofs, certificate-backed results, bounded searches, conditional statements and open work. Paper I is public; the full laboratory remains private.
Current frontier
Proved, excluded, and open.
Proved reductions
Selected formal reductions, including square-middle representations and forward projections into curve models. Each result has its own direction and hypotheses.
Excluded subfamilies
Selected infinite subfamilies, including fixed-parameter cases. Excluding such a family does not exclude all other cases or establish a percentage of progress towards the full conjecture.
Open remainder
Many branch-specific exclusion, reconstruction and finiteness theorems, and the combination of the branch results into a proof of the full conjecture. The remaining work is not just final bookkeeping.
What counts as progress
A proved reduction, a theorem or a precisely checked finite result.
Useful results include a proved necessary condition, a source-equivalent reformulation, an explicit construction, an infinite-family exclusion or a theorem that reduces a question to finitely many cases. A bounded search is reported at its actual bound. A promising curve model remains a research tool until the needed argument is complete.
A source solution may justify an auxiliary point without every auxiliary point reconstructing a source solution. Likewise, one excluded subfamily does not close its parent branch. These distinctions are kept in the theorem statements rather than left to interpretation.
The research system
Human-led, AI-assisted mathematical research.
Large language models assist with literature search, conjecture generation, implementation, formalisation and adversarial review. Human judgement selects the research direction and approves the scope of public claims. Lean checks formal proofs; exact computations and counterexamples support the relevant mathematical work. Contribution, verification and release decisions remain distinct.
Further mathematical records
Public Paper I and further material on request.
Wider representation definitions, hypotheses and proved directions beyond Paper I On request
Full laboratory theorem inventory and open proof obligations On request
Paper I public repository and proof material at v1.0.0 →Reproducibility and auditability across Overdog →Request the current material →