福建
维恩图，几乎每个人都在课本上见过：几个相互交叠的圆圈，清楚地展示集合之间的关系。两三个圈的版本，小学生都能画出来。
可一旦圆圈增加到十几个，并且要求图形旋转后仍完全对称，这个看似简单的问题就会变成数学家的噩梦。
最近，研究者克里斯·佐巴在预印本平台arXiv上发表论文，宣布构造出由17条和19条曲线组成的简单旋转对称维恩图。
整个搜索过程由两套AI系统完成，分别是Anthropic公司的Claude与OpenAI公司的Codex。它们在佐巴的指导下，只用了五天时间。
这一成果把简单对称维恩图的纪录，从13条曲线一举推进到了19条曲线。
一个圈套一个圈的数学难题
维恩图由英国逻辑学家约翰·维恩于1880年提出。用n条闭合曲线画出的维恩图，必须完整呈现全部2的n次方种交叠组合，每个区域都要存在且连成一片。
通常，三个圆就能画出完美的三集合维恩图，但到了四个集合，圆形便已无能为力。
对17条曲线来说，这意味着要容纳131072个区域；到了19条曲线，区域数更是高达524288个。
要让这十几万个区域一个不少、一个不重地安排妥当，同时保证图形对称，难度可想而知。
数学家追求的不只是“画得出”，还要“画得美”。所谓旋转对称，是指把图形绕中心转动一定角度后，所有曲线恰好互相重合，宛如一朵层层绽放的玫瑰。
早已证明，这种对称维恩图只可能出现在曲线数为质数的情形。2004年，美国数学家格里格斯、基利安和萨维奇进一步证明，每个质数都存在对称维恩图。
这是因为对称性要求每一类交叠区域的数量都能被曲线数整除，而只有质数能满足这一苛刻条件。
但他们构造的图形中，许多曲线挤在同一点交叉，算不上“简单”。所谓简单，是要求每个交点只有两条曲线穿过。
此前，简单对称维恩图的纪录停留在13条曲线，由加拿大学者在2014年前后找到。
再往前追溯，英国统计学家爱德华兹曾在上世纪末构造出7条曲线的对称维恩图，被视为这一领域的经典之作。
AI如何找到“玫瑰”
新研究的突破，来自一种别出心裁的随机搜索策略。它并不追求一步到位，而是允许在探索中犯错。
AI从格里格斯等人的经典图形出发，先拆开多条曲线交于一点的地方，再在保持旋转对称的球面网格上进行随机游走。
随机游走就像在迷宫中一边摸索一边记录，好的方向保留，坏的方向舍弃。
这种方法允许某些区域在搜索途中暂时“重复出现”。就像拼图时先容忍几块错位，再一点点调整到位。
最终，研究找到了4个17曲线图和9个19曲线图。这些图形的数据和搜索代码均已公开。
每一个图形都像一朵繁复的曼陀罗，曲线层层缠绕，却在旋转之下保持完美的秩序。
关键在于，这些图形全都是“非单调”的。这正是过去依靠交叉序列搜索的方法始终找不到它们的原因。
所谓单调，大致是指每个区域都能找到恰好多一条或少一条曲线覆盖的相邻区域，层次分明地递进。非单调图形打破了这种规整次序，也就更难被捕捉。
研究顺带还找到了首批非单调的11曲线和13曲线简单对称维恩图，为这一领域打开了新的视野。
机器验证给出“铁证”
如此复杂的图形，人眼根本无从核对，那么如何确信它是对的？答案是：交给机器来检查。
论文为每个图形都附上了可由计算机核查的“证书”，并配备独立的检查程序。其中17曲线和19曲线各有一个证书，还通过了Lean 4定理证明器的形式化验证。
这意味着，结论不依赖于对AI的信任，而是经过了严格的逻辑检验。即便是怀疑AI的人，也可以亲自验证结果。
形式化验证的意义在于，每一步推理都由计算机逐条检查，几乎杜绝了人为疏漏。
佐巴还在论文中详细披露了两套AI系统各自承担的角色，以呼应数学界今年提出的关于人工智能与数学的《莱顿宣言》。
在AI垃圾论文泛滥、数学界对AI心存疑虑的当下，这项工作提供了另一种样本：透明的分工、可复现的代码，以及无可辩驳的机器证明。
与那些难以理解的AI证明不同，这项成果的每个图形都可以被任何人下载、复核和重现。
当然，这只是针对两个具体数字的构造，而非适用于所有质数的一般定理。更大规模的简单对称维恩图是否存在，仍是悬而未决的谜题。
但这些由AI“画”出的数学玫瑰已经证明，在浩瀚的组合空间里搜寻答案，机器正成为数学家越来越得力的伙伴。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
