AI 中文总结
本文给出一个初等证明，证明每个分母无平方因数的正有理数可表示为不同单位分数（分母为两个不同素数乘积）的有限和，解决了 Erdős 问题 #306，并已在 Lean 4 中形式化。
AI 中文摘要
我们给出一个初等证明，证明每个分母 $b$ 为无平方因数的正有理数 $a/b$ 都是不同的单位分数 $1/n$ 的有限和，其中每个 $n$ 是两个不同素数的乘积（Erdős 问题 #306）。在化简到小目标之后，我们取一个位于 $(y^2,2y^2]$ 中的素数之间的完全二分图，连同 $2$ 和 $b$ 的素数，以及 $(y^8,y^9]$ 中素数的一个经过调校的初始段，并证明某个子图具有与 $a/b$ 模 $1$ 同余的倒数和；小的总质量随后迫使等式成立。将这种子图的数目写成有限傅里叶和，我们使用一个由图的两侧索引的表格将频率分为三种情况。小的整数频率给出一个正的主项，而所有其他频率通过一个除数计数论证和一个无环绕形式的中国剩余定理而可忽略。关于素数的唯一输入是 Chebyshev 型界。圆法框架来自 Tang 的 Lean 开发，该开发给出了第一个证明；我们的构造移除了其锚点同步步骤。该证明已在 Lean 4 中形式化，除了一条引用的 Ramanujan 不等式。这项工作是一次人机协作：AI 工具在构造、实验和写作方面做出了实质性贡献。
英文摘要
We give an elementary proof that every positive rational number $a/b$ with $b$ squarefree is a finite sum of distinct unit fractions $1/n$, where each $n$ is a product of two distinct primes (Erdős Problem #306). After a reduction to small targets, we take a single complete bipartite graph between the primes in $(y^2,2y^2]$, together with $2$ and the primes of $b$, and a tuned initial segment of the primes in $(y^8,y^9]$, and show that some subgraph has reciprocal sum congruent to $a/b$ modulo $1$; the small total mass then forces equality. Writing the number of such subgraphs as a finite Fourier sum, we sort the frequencies into three cases using a table indexed by the two sides of the graph. The small integer frequencies give a positive main term, and all other frequencies are negligible by a divisor-counting argument and a no-wrap-around form of the Chinese remainder theorem. The only inputs about primes are Chebyshev-type bounds. The circle-method framework comes from Tang's Lean development, which gave the first proof; our construction removes its anchor-synchronisation step. The proof has been formalised in Lean 4, apart from a cited inequality of Ramanujan. This work is a human-AI collaboration: AI tools contributed substantially to the construction, the experiments and the writing.
Comments13 pages. Lean 4/Mathlib formalisation included as ancillary files (anc/lean)
