AI Proof WatchKeep up with AI contributions

Nonquadraticity of Lambert Series Values

Costa Lambrinoudis

For F(q)=Σₙ≥₁1/(qⁿ−1), a degree criterion excludes polynomial relations of degree at most e over Q(q) when eλ log M(q)<log q, where λ=(42963+428220/π²)/202140. It gives nonquadraticity for every integer q≥2 and irrationality for rational q=a/b>1 when log b/log a<0.5728; a certified refinement reaches 0.573290.

Sources for this record

What was already known

Erdős proved irrationality at integer bases. Earlier rational-base thresholds were about 0.3987 and 0.405683.

AI involvement AI-led

Costa Lambrinoudis directed and supervised the work. The repository credits generative AI with nearly all mathematical arguments, manuscript writing and Lean formalization; it does not name the model.

The author explicitly credits AI with nearly all retained mathematics and Lean work under his direction; the exact model identity is unreported.

Importance Notable

Extends the proven irrationality region and establishes integer-base nonquadraticity.

Limitations

Erdős Problem 1049 remains open at q=3/2. The source reports a complete Lean build and certificate generation; no independent human mathematical check is documented.

Technical verification Formal (Lean 4.33.1 kernel with Mathlib, axiom audit and exact refinement certificates)

The repository reports complete Lean/Mathlib formalization with no additional axioms or admitted proofs; its verification guide maps the degree criterion, integer nonquadraticity and 0.5728/0.573290 rational-region results to declarations and gives build, axiom-audit and kernel-replay commands. VibeMathed reports inspecting the statements and regenerating the refinement certificate, and documents the checking scope.

Formal checking

The repository reports complete Lean/Mathlib formalization with no additional axioms or admitted proofs; its verification guide maps the degree criterion, integer nonquadraticity and 0.5728/0.573290 rational-region results to declarations and gives build, axiom-audit and kernel-replay commands. VibeMathed reports inspecting the statements and regenerating the refinement certificate, while the full build was not rerun in this review.

Checker
Lean kernel and verification scripts in Lambrinoudis's repository
Scope
Degree-exclusion theorem, integer-base nonquadraticity, rational-base irrationality below 0.5728 and refined certified region below 0.573290
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Default for missing evidence of a person's understanding of the central determinant argument: the explanation and manuscript are credited largely to AI, and human supervision alone does not establish it.

Correction and publication history