Source arithmetic
Powerful numbers on the integer line, source cases and canonical normal forms. Kernels, prime valuations and congruence conditions expose restrictions before a change of representation.
Erdős Basecamp
Powerful numbers, exact computation and proof.
Can three consecutive positive integers all be powerful? The pair 8 = 23 and 9 = 32 is powerful; 10 = 2 × 5 is not, because its prime factors appear only once. Erdős Basecamp studies E364 and related integer problems through exact arithmetic, alternative representations and proof.
One current public result, the 17/41 obstruction, excludes infinite families in a specified recurrence setting. The full Erdős 364 conjecture remains open.
Current public result
Erdős 364 and the 17/41 result
E364 is the concrete powerful-number problem within Basecamp. Paper I supplies a public partial result, with an explanation, an animation and a versioned article and source release.
Paper I excludes indices divisible by 17 or 41 in a shifted-square Lucas-sequence family under stated hypotheses. This excludes infinite families, not the full problem. Erdős problem 364 remains open.
The proof makes multiple exact descriptions of the same candidate meet. An obstruction at fixed indices 17 and 41 then propagates to infinitely many indices, rather than relying on a larger search.
The exact statement and square-middle scope come before the wider methods. Other project-reported reductions require their individual records; Paper I is not a proof of the whole programme.
Mathematical approaches
Three ways into an integer problem
Start with source arithmetic, find a representation that exposes structure, and prove the conclusion it supports. These approaches serve E364 and the wider mathematics programme.
Alternative representations
Pell and coupled Pell-type equations, Lucas and Chebyshev recurrences, quartic and Mordell-type curves, genus-two curves, number fields and local-symbol constructions. Exact finite certificates support specific steps.
Proof and exclusion
Necessary conditions, sufficient constructions and equivalences have different jobs. Local obstructions, fixed-prime arguments, subfamily exclusions, theorem-bounded finite checks and Lean proofs must each establish a stated conclusion.
A change of representation can make an arithmetic problem easier to analyse. The required argument depends on the conclusion: constructing an original solution needs a reconstruction argument, while ruling out original solutions can require only a proved necessary condition and an exclusion of the auxiliary solutions. Selected reductions are reported by the project; their exact statements and source records must be inspected individually.
- State the original problem and assumptions.
- Map into an auxiliary representation.
- Prove the implication needed to transfer the conclusion.
A forward map and the implication needed to transfer a conclusion require separate arguments. This illustration does not assert a new theorem or a solution to problem 364.
Basecamp is the mathematics programme inside ORBIT's Theorems direction. Computation, formalisation and conjectural structure have distinct roles, authority and failure modes.
Proof and computation
What the mathematical evidence establishes
A counterexample refutes a conjecture. Finding none in a finite search leaves the unsearched cases open. A proof establishes a precise statement under its hypotheses; a pattern can guide the next question.
Bounded computation
Searches are useful when their domain, inputs, code and conclusion are explicit. Preserve provenance, assumptions, negative results and replay paths. A large bound alone does not turn a search into a general theorem.
Formal statements
Lean and typed proof artefacts make definitions, dependencies and assumption boundaries inspectable. They clarify which conjecture, lemma or theorem is being checked, separately from its implementation.
For Paper I, Lean covers the integer-Jacobi and recurrence exclusions and propagation, not the human Hilbert-reciprocity, maximality or Pell arguments.
Search discipline
The interesting part is not only whether a computation succeeds. It is what the computation reveals about the structure of the remaining problem. A finite check can complete a theorem-bounded remainder or verify a fixed certificate; an exploratory search has a different role.
Papers and source
Inspect a result without taking a programme tour
Use the public article for exact hypotheses and proofs, the tagged source for formal and computational records, and the E364 page for the open remainder.
Paper I articlePublic v1.0.0 release and exact theorem statementsProof and computation recordsTagged source, dependencies and disclosed gapsE364 proof coveragePublic result, project-reported reductions and open obligationsBridgeExact and empirical asymmetryMethodClaim-limited publicationCataloguePublications and source artefacts
The long-form illustrated guide belongs with the explanation; it is not a separate result. Read or watch for understanding, then use the article and source to inspect the claims. The release discloses three unrecovered historical Magma inputs; public secondary checks do not fill that provenance gap.
The Rosetta Stone hypothesis asks whether exact mathematical asymmetries have a useful relationship to empirical drift signals. That cross-programme translation has not been established.