AI 中文总结
该研究完成了“素数集合是超自然的”猜想的Lean 4形式化，将其表述为开放问题，为自动推理系统提供了可验证的精确证明目标。
AI 中文摘要
论文《猜想：素数集合是超自然的》提出猜想：不存在由恒等函数和常数通过有限次逐点加法、乘法、指数运算构造的非常数函数，能将每个正整数映射为素数。我们在Mathlib上完成了该论文的完整Lean 4形式化：每个定义、示例、备注、编号结果及实验表格行都有经机器验证的对应内容，无“sorry”。该猜想及其推广被明确表述为命名的开放问题，由此成为精确目标，自动推理系统现在可尝试生成经内核验证的证明。
英文摘要
The paper \emph{Conjecture: the set of prime numbers is supernatural} conjectures that no non-constant function built from the identity and constants by finitely many pointwise additions, multiplications, and exponentiations maps every positive integer to a prime. We give a complete Lean~4 formalization of that paper over Mathlib: every definition, example, remark, numbered result, and experimental table row has a machine-checked counterpart, with no \lcode{sorry}. The conjecture and similar generalizations are stated exactly, as named open problems. So stated, the conjecture becomes a precise target: an automated reasoning system can now attempt a kernel-checked proof.
