Formal Conjectures contributions

Merged mathematical contributions

#5034 · Add formal proof for Erdős Problem 258 constant-base variant

Proof link for the constant-base variant of Erdős’s 1948 theorem.

Merged 2026-09-18.

Latest individual review: approved on an earlier head, 2026-09-18.

#6505 · Erdős 1041: mark solved with answer(False) and link a formal proof

Negative answer to the exact formal path-image statement, credited to ani; independent correspondence review of the 1958 wording remains separate.

Merged 2026-09-23.

Latest individual review: approved on current head, 2026-09-23.

#6506 · Erdős 257: link a formal proof of variants.tsum_top

Proof link for the full-support variant of Erdős’s 1948 theorem; arbitrary infinite supports remain open.

Merged 2026-09-23.

Latest individual review: approved on current head, 2026-09-23.

#6507 · Erdős 1049: link a formal proof of variants.geq_2_integer

Proof link for integer bases at least two, following Erdős’s 1948 theorem; general rational bases remain open.

Merged 2026-09-23.

Latest individual review: approved on current head, 2026-09-23.

#6529 · Erdős 257: add the reciprocal-summable support variant

Erdős’s classical coprimality-free result: an infinite support with summable reciprocals gives an irrational series at every integer base at least two. The merged subtype formulation links its verified adapter; the unrestricted question remains open.

Merged 2026-10-09.

Latest individual review: approved on an earlier head, 2026-10-08.

Open requests

#6522 · Set Erdős 269 rationality variant to false

Literature-backed negative answer to universal rationality using Steve Fan’s two-prime argument. No formal transcendence proof claimed; universal irrationality remains open.

Open; aggregate review decision: review required.

Latest individual review: approved on current head, 2026-10-06.

#6523 · Erdős 243: add cubic-rate irrationality and slow-growth rigidity

Cubic-rate irrationality and slow-growth rigidity under additional growth and increment hypotheses; the original question remains open.

Open; aggregate review decision: review required.

Latest individual review: commented on an earlier head, 2026-10-06.

#6527 · Erdős 1049: add rational-base contour and irrationality exponent bound

A strict logarithmic contour, all positive powers and an irrationality-exponent bound; the general rational-base question, including 3/2, remains open.

Open; aggregate review decision: review required.

Latest individual review: approved on current head, 2026-10-06.

#6528 · Erdős 257: add weighted and mixed-support irrationality variants

Irrationality under sufficient weighted support and covering hypotheses, not for arbitrary infinite supports.

Open; aggregate review decision: review required.

Latest individual review: commented on an earlier head, 2026-10-06.

#6576 · Erdős 1041: add sharp normalized collinear gap variant

Sharp product-height bound for normalized real roots and a whole adjacent interval; separate from the merged negative answer for general paths.

Open; aggregate review decision: review required.

Latest individual review: commented on an earlier head, 2026-10-06.

#6577 · Erdős 249: add countable least-residue dilation independence

Rational linear independence of 1 and the countable dilation family for fixed modulus at least three and integer base at least two; the unreduced totient question remains open.

Open; aggregate review decision: review required.

Latest individual review: approved on current head, 2026-10-06.

#6579 · Erdős 249: classify rational dyadic totient observables

For rational-valued observables modulo 2^k, the binary series is rational exactly when the observable is constant on even residue classes.

Open; aggregate review decision: review required.

Latest individual review: approved on an earlier head, 2026-10-06.

#6780 · Add fixed-base geometric-moment Hankel asymptotic

Asymptotic for each fixed 0 < q < 1; no uniformity as q approaches one and no solution of #1049.

Open; aggregate review decision: review required.

Latest individual review: commented on current head, 2026-10-07.

Proof-link maintenance

#6971 · Update four proof links to kernel-checked sources

Updates four already accepted proof links to immutable sources checked by Lean and NanoDa in the cited Palomar runs. This maintains their evidence links; it adds no new mathematical result.

Open; aggregate review decision: review required.

Authorship and closed requests

#6578 · Add Will Cook to AUTHORS

Administrative attribution: adds Will Cook to AUTHORS; excluded from the mathematical contribution count.

Merged 2026-09-24.

Latest individual review: approved on current head, 2026-09-24.

Exact target names, reviewed commits and observation fields are recorded in the crosswalk source. Open the linked request for subsequent activity.

Erdős #68

Local question: Is the series sum_{n >= 2} 1/(n! - 1) irrational?

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_68 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos68.erdos_68 at FormalConjectures/ErdosProblems/68.lean:33; proof status sorry.

• Statement scope: The same displayed factorial-denominator irrationality question.

• Indexing: Formal Conjectures sums over n : Nat after the explicit shift n + 2; the displayed local question sums over integers n >= 2.

• Casts and ambient types: The summand is explicitly real after casting (n + 2).factorial into Real in the denominator.

• Answer/proof status: The upstream declaration uses answer(sorry) and its proof is sorry; it is statement prior art, not proof authority.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #243

Local question: Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually?

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_243 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos243.erdos_243 at FormalConjectures/ErdosProblems/243.lean:38; proof status sorry.

• Statement scope: The rapid-growth, rational reciprocal-sum, eventual-Sylvester question is represented, but the local work proves only conditional state-system consequences.

• Indexing: The upstream sequence is zero-based and refers to a (n - 1), using truncated Nat subtraction; comparison with a traditional sequence starting at a_1 requires discarding a finite prefix.

• Casts and ambient types: The growth limit is Real-valued, while ha₂ is Summable for a Rational-valued reciprocal sequence. This asserts a Rational sum exists and must be related explicitly to a Real rationality premise.

• Answer/proof status: The open theorem has a sorry proof and no answer wrapper; the conclusion is an eventual filter statement.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #249

Local question: Is the binary Lambert series sum phi(n)/2^n irrational?

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_249 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos249.erdos_249 at FormalConjectures/ErdosProblems/249.lean:35; proof status sorry.

• Statement scope: The binary totient-series irrationality question is represented; neither corpus solves it.

• Indexing: Formal Conjectures sums from n = 0. The n = 0 totient term is zero, so the displayed positive-index series is expected to agree, but this crosswalk contains no Lean reindexing proof.

• Casts and ambient types: Irrational forces a Real-valued sum and Lean inserts coercions for Nat totients and powers; the surface syntax leaves those casts implicit.

• Answer/proof status: The upstream declaration uses answer(sorry) and its proof is sorry.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #251

Local question: Is the dyadic series of consecutive primes irrational? Equivalently, is the corresponding consecutive-prime-gap dyadic series irrational?

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_251 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos251.erdos_251 at FormalConjectures/ErdosProblems/251.lean:31; proof status sorry.

• Statement scope: The same dyadic prime-series irrationality question is represented.

• Indexing: Nat.nth Nat.Prime is zero-based and the denominator is 2^n. Relative to the displayed convention p_1 / 2^1 + p_2 / 2^2 + …, the upstream value is multiplied by 2; irrationality should be invariant under that nonzero rational factor, but no adapter theorem is recorded here.

• Casts and ambient types: The prime and power expressions are Nat-valued surface syntax coerced into the Real-valued sum required by Irrational.

• Answer/proof status: The upstream declaration uses answer(sorry) and its proof is sorry.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #257

Local question: Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational?

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_257 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos257.erdos_257 at FormalConjectures/ErdosProblems/257.lean:35; proof status sorry.

• Statement scope: The upstream open theorem quantifies over every infinite Nat support. The local expansion studies the same positive-exponent Mersenne support problem without proving the universal endpoint.

• Indexing: The upstream support may contain exponent zero. Its n = 0 summand is 1 / 0 = 0 under Lean’s division convention, so zero is analytically invisible; a formal adapter must still normalize Set Nat and subtype indexing explicitly.

• Casts and ambient types: The denominator power is inferred in Real from the explicit numerator cast. The solved variant instead sums Nat divisor counts coerced to Real.

• Answer/proof status: The universal theorem and solved-variant irrationality theorem are sorry; the Lambert identity tsum_top_eq is proved upstream.

• Conservative verdict: adapter_checked_against_pinned_statement.

• Machine-checked equivalence: Erdos249257.FormalConjecturesAdapter.erdos_257_variants_tsum_top in adapters/FormalConjecturesAdapter.lean, checked in this repository at leanprover/lean4:v4.29.1, and independently at Formal Conjectures’ own leanprover/lean4:v4.27.0 with the corpus theorems supplied as axioms so that the bridge alone was checked; axioms propext, Classical.choice, Quot.sound.

• Historical adapter-admission record: submitted_upstream. See contribution activity for upstream lifecycle.

Erdős #269

Local question: For a finite set of at least two primes, is the sum of reciprocals of the running least common multiples of the smooth numbers irrational? This library treats the three-prime case.

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_269 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos269.erdos_269.variants.irrational at FormalConjectures/ErdosProblems/269.lean:73; proof status sorry.

• Statement scope: Formal Conjectures states finite-prime rational and irrational variants and an infinite-prime theorem. The local programme proves only subsidiary structure for the three-prime case.

• Indexing: The upstream series includes n = 0 and its empty-prefix lcm term; comparison with a convention beginning at the first nonempty prefix differs by a finite rational normalization that is not formalized here.

• Casts and ambient types: partialLcm is Nat-valued and coerced into a Real reciprocal. The rational variant expresses rationality using existence of q : Rational equal to the Real series through coercion.

• Answer/proof status: All three upstream research endpoints have sorry proofs; none is proof authority for the local results.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #1041

Local question: Must two roots of a monic polynomial in the open unit disc be joined by a sub-two-length curve inside its unit lemniscate? Ani’s degree-seven example refutes the exact Formal Conjectures statement; correspondence with the 1958 wording awaits human review.

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_1041 (canonical problem packet); Returns the local problem packet with the exact Formal Conjectures Hausdorff refutation, credited source, papers, declarations and historical-review boundary.

• Upstream declaration: Erdos1041.erdos_1041 at FormalConjectures/ErdosProblems/1041.lean:67; proof status sorry.

• Statement scope: The local Hausdorff theorem refutes the exact Formal Conjectures path-image-length proposition for ani’s degree-seven polynomial. The 1958 curve-length wording remains a separate historical correspondence audit.

• Indexing: There is no series indexing issue. The upstream theorem quantifies polynomial degree n >= 2 and selects roots through multiset containment, including multiplicity.

• Casts and ambient types: Both formal statements use a Complex path whose image lies in the strict unit lemniscate; length is one-dimensional Hausdorff measure of Set.range γ in ENNReal. The older local total-variation theorem is separate.

• Answer/proof status: At the pinned snapshot, the upstream declaration has answer(sorry) and a sorry proof. Local Lean proves the exact Hausdorff negation and answer(False) form. The later answer correction merged as PR #6505; independent historical adjudication remains unrecorded.

• Conservative verdict: statement_level_alignment_only.

• Machine-checked equivalence: none.

• Local refutation: Erdos1041.Counterexample.erdos1041_hausdorff_negation and Erdos1041.Counterexample.erdos1041_hausdorff_answer_false at 7380b7871687b6bcc41ca0143c61f232e8af6500; ani, erdosproblems.com forum thread 1041, 7 September 2026. Exact Formal Conjectures path-image formulation refuted; independent review of correspondence with the 1958 wording remains open.

• Historical adapter-admission record: not_ready_to_submit. See contribution activity for upstream lifecycle.

Erdős #1049

Local question: For which rational bases is the corresponding series irrational? The first resistant explicit base is three halves.

• Canonical local return route: python3 scripts/query_corpus.py --route erdos_1049 (canonical problem packet); Returns the local problem packet with result families, declarations, papers and sources, and the exact open boundary.

• Upstream declaration: Erdos1049.erdos_1049 at FormalConjectures/ErdosProblems/1049.lean:40; proof status sorry.

• Statement scope: The upstream open theorem asks for every rational t > 1. The local programme does not prove that endpoint, but its full-support theorem covers positive integer bases and may discharge the upstream solved integer-base variant after adapters.

• Indexing: The upstream sums use positive naturals. The local full-support theorem uses k : Nat with exponent k + 1; an explicit equivalence between those index types is required.

• Casts and ambient types: The upstream open base is Rational and the solved variant is Integer, both cast into Real powers. The local theorem takes b : Nat and casts it to Real, so Integer-to-Nat and cast/power normalization must be checked.

• Answer/proof status: The rational-base conjecture and integer-base variant have sorry proofs. The upstream Lambert identity is proved, including branches outside the t > 1 problem regime that rely on Lean’s nonsummable-tsum convention.

• Conservative verdict: adapter_checked_against_pinned_statement.

• Machine-checked equivalence: Erdos249257.FormalConjecturesAdapter.erdos_1049_variants_geq_2_integer in adapters/FormalConjecturesAdapter.lean, checked in this repository at leanprover/lean4:v4.29.1, and independently at Formal Conjectures’ own leanprover/lean4:v4.27.0 with the corpus theorems supplied as axioms so that the bridge alone was checked; axioms propext, Classical.choice, Quot.sound.

• Historical adapter-admission record: submitted_upstream. See contribution activity for upstream lifecycle.

Erdős #257: Erdos257.erdos_257.variants.tsum_top

The upstream proposition is stated verbatim in the adapter and derived from this library. This local check is separate from the dated contribution and review record above.

Local evidence:

• irrational_erdosSum_full_support in Erdos249257/CertificateKernel.lean:8328
• irrational_erdosBorwein_series in Erdos249257/CertificateKernel.lean:8335

Unproved bridge obligations:

• Relate the upstream Nat-indexed Lambert series, whose n = 0 term is zero, to the local successor-indexed base-2 series.
• Transport irrationality through the upstream proved divisor-sum identity without importing a proof-incompatible local environment.
• Review theorem attribution, contribution scope, licensing, automation disclosure, and upstream contribution policy with a human before any patch is prepared.

Erdős #1049: Erdos1049.erdos_1049.variants.geq_2_integer

The upstream proposition is stated verbatim in the adapter and derived from this library. This local check is separate from the dated contribution and review record above.

Local evidence:

• irrational_erdosSum_full_support in Erdos249257/CertificateKernel.lean:8328

Unproved bridge obligations:

• Convert t : Integer with t >= 2 to a natural base and prove all Integer/Nat/Real cast and power identities used by the target.
• Reindex the positive-natural upstream sum to the local Nat successor sum.
• Confirm that the proof uses only upstream-compatible imports and does not accidentally rely on the irrelevant nonsummable branches of the upstream Lambert identity.
• Review theorem attribution, contribution scope, licensing, automation disclosure, and upstream contribution policy with a human before any patch is prepared.

Upstream #258: Erdos258.erdos_258.variants.constant

• Recorded here because: This library does not work on Erdos #258, so an index keyed by local problem number had nowhere to put this match and did not record it. The upstream statement is the same mathematics as the #257 and #1049 targets in a third coefficient convention.
• Machine-checked equivalence: Erdos249257.FormalConjecturesAdapter.erdos_258_variants_constant in adapters/FormalConjecturesAdapter.lean, checked in this repository at leanprover/lean4:v4.29.1, and independently at Formal Conjectures’ own leanprover/lean4:v4.27.0 with the corpus theorems supplied as axioms so that the bridge alone was checked; axioms propext, Classical.choice, Quot.sound.
• Historical adapter-admission record: submitted_upstream; upstream lifecycle is recorded above.