OpenConjecture

OpenConjecture是一个从arXiv数学页面发布的论文中提取开放猜想并构建的数据集。数据集包含890个（可能开放的）猜想，来自当前arXiv数学公告流中的6661篇论文。每个猜想都通过LLM标记了其有趣性和可解性，并使用GPT-5.4尝试对最易解的猜想进行证明。

OpenConjecture is a dynamic dataset that extracts open conjectures from papers published on arXiv's mathematics section. This project uses LLMs to annotate each conjecture with its interest level and solvability, and attempts to prove the most tractable conjectures using GPT-5.4 Thinking. Currently, the dataset contains 890 (potentially open) conjectures sourced from 6661 mathematics papers on arXiv.

原始信息汇总

OpenConjecture 数据集概述

数据集简介

OpenConjecture 是一个从 arXiv 数学版块论文中提取开放猜想并构建的持续更新的数据集。该项目使用大型语言模型（LLM）对每个猜想的趣味性和可处理性进行标注，并尝试对最具可处理性的猜想进行证明。

数据规模与来源

• 数据来源：arXiv 数学版块近期发布的论文。
• 论文数量：6661 篇。
• 猜想候选数量：1075 个。
• 标注为真实开放猜想数量：890 个。
• 标注为非真实猜想数量：182 个。
• 标注为不确定数量：3 个。
• 主要论文发布时间范围：2026年2月2日至2026年3月16日。
• 当前数据集快照文件：data/conjectures_month_live_20260317.sqlite。

数据处理流程

1. 数据获取：获取指定日期范围内 arXiv 数学版块的论文公告。
2. 猜想提取：从论文中提取猜想块，并与论文元数据（包括 arXiv 类别、DOI、期刊引用、评论和许可证）一起存储。
3. 猜想标注：使用 GPT-5 Mini 将提取的候选猜想标注为 real_open_conjecture、not_real_conjecture 或 uncertain，并对真实猜想进行 interestingness（趣味性）和 viability（可处理性）评分。
4. 求解尝试：（可选）使用 GPT-5.4 Thinking（xhigh）尝试对最具可处理性的猜想子集进行求解。
5. 形式化验证：（可选）使用 Lean 对步骤（4）中的求解尝试进行形式化。

求解器试点结果

当前 GPT-5.4 求解器试点对 20 个最高优先级的可行猜想进行了尝试，结果如下：

• 6 个强解决质量结果：2 个确认，4 个否定。
• 2 个规范/形式化问题。
• 3 个部分进展结果。
• 1 个有条件确认。
• 1 个实质上已解决的草案问题。
• 7 个未解决结果。 注意：这些是模型报告的结果，并非经过独立验证的数学证明或反例。

形式化验证

使用 Codex（配合 GPT-5.4）尝试将 20 个证明尝试中的 6 个在 Lean 中进行形式化。

• 形式化尝试数量：6 个。
• 系统报告成功数量：4 个。
• 形式化尝试时间：从数小时到超过 30 小时不等。 注意：这些形式化尝试由 LLM 生成并由模型报告，尚未经过独立验证。

相关文件

• 求解器尝试摘要：data/exports_solver_status_20260309_attempts20/solver_attempts_20_summary.md
• 求解器尝试审计：data/exports_solver_status_20260309_attempts20/solver_attempts_20_audit.md
• 求解器尝试数据：data/exports_solver_status_20260309_attempts20/solver_attempts_20.csv
• 形式化验证工作区：formalization/
• 形式化验证说明：formalization/README.md

项目结构

主要模块包括：

• CLI 入口点：src/conjectures_arxiv/cli.py
• 处理流程编排：src/conjectures_arxiv/pipeline.py
• arXiv API 客户端：src/conjectures_arxiv/arxiv_client.py
• 数据提取与标注：src/conjectures_arxiv/conjecture_extractor.py、src/conjectures_arxiv/llm_filter.py
• 求解器：src/conjectures_arxiv/solver.py
• 数据库与导出：src/conjectures_arxiv/database.py
• 发布模块：src/conjectures_arxiv/hf_publish.py、src/conjectures_arxiv/s3_publish.py

搜集汇总

数据集介绍

构建方式

在数学研究领域，开放猜想构成了理论进展的重要驱动力。OpenConjecture数据集通过自动化流程从arXiv数学版块的近期论文中系统性地提取开放猜想。该流程首先获取指定时间范围内的论文元数据，随后利用自然语言处理技术识别并抽取出猜想文本块，并辅以论文的类别、DOI、期刊引用等元信息。每个候选猜想经由大型语言模型GPT-5 Mini进行标注，分类为真实开放猜想、非真实猜想或不确定状态，并对真实猜想的有趣性和近期可解性进行评分，从而构建出一个结构化的、动态更新的猜想知识库。

特点

该数据集的核心特征在于其动态性与深度加工。它不仅收录了来自数千篇近期数学论文的数百个开放猜想，还通过大型语言模型对每个猜想进行了多维度的智能标注，包括有趣性与可解性评估。更独特的是，项目尝试使用GPT-5.4 Thinking模型对部分高可解性猜想进行证明或证伪的探索，并初步利用Codex与GPT-5.4协作，将部分证明尝试形式化于Lean定理证明器中。这种从原始文本提取到高级逻辑验证的递进式处理，使数据集超越了简单的文本集合，具备了支持自动化推理研究的潜力。

使用方法

研究人员可通过命令行工具灵活地使用该数据集。初始化数据库后，用户可指定日期范围从arXiv导入论文数据，并运行过滤流程利用GPT-5 Mini对提取的猜想进行标注与评分。对于筛选出的高优先级猜想，可进一步调用GPT-5.4模型尝试求解。数据集支持以SQLite、CSV等多种格式导出，并可发布至Hugging Face平台共享。项目还提供了独立的Lean形式化工作区，供用户深入验证或完善模型生成的证明。整个流程为数学猜想发现、评估乃至自动化证明研究提供了端到端的实验框架。

背景与挑战

背景概述

在数学研究领域，开放猜想的系统化收集与分析长期面临数据分散与形式化不足的挑战。OpenConjecture数据集应运而生，该项目由研究团队于2026年创建，旨在通过自动化流程从arXiv数学预印本平台实时提取开放猜想，并利用大型语言模型进行标注与验证。其核心研究问题聚焦于构建一个动态、可计算的数学猜想知识库，以探索人工智能辅助数学发现的潜力。该数据集通过整合论文元数据、猜想可解性评估及形式化证明尝试，为数学与人工智能的交叉研究提供了新颖的实验平台，有望推动自动推理与交互式定理证明领域的发展。

当前挑战

OpenConjecture数据集致力于解决数学猜想自动化发现与验证的领域挑战，其核心在于从非结构化文本中精准识别开放猜想，并评估其可解性。构建过程中的主要挑战包括：首先，从arXiv论文中可靠地提取猜想陈述，需克服自然语言表达的多样性与模糊性；其次，利用大型语言模型进行标注时，需确保‘趣味性’与‘可解性’评分的客观性与一致性；再者，将模型生成的证明尝试形式化为Lean代码，涉及高昂的计算成本与验证复杂性，且当前结果尚未经过独立数学验证，其可靠性仍待严格审查。

常用场景

经典使用场景

在数学研究领域，OpenConjecture数据集为学者提供了一个动态更新的开放猜想库，其经典使用场景在于支持自动化的猜想分析与验证流程。研究人员可以借助该数据集，系统性地筛选近期arXiv数学预印本中提出的未解决问题，并利用大型语言模型对猜想的趣味性与可解性进行初步评估，进而引导后续的形式化证明尝试。这一场景不仅加速了数学发现的进程，也为计算辅助证明提供了结构化数据基础。

实际应用

在实际应用中，OpenConjecture数据集可服务于数学教育、研究工具开发及学术出版等多个领域。教育机构能利用其筛选适合学生探讨的猜想案例，增强探究式学习体验；开发者则可基于该数据集构建智能证明辅助系统，为数学家提供猜想验证的初步参考；同时，期刊与会议也能借助其追踪领域进展，优化审稿流程。这些应用彰显了数据驱动方法在现代数学实践中的渗透力。

衍生相关工作

围绕OpenConjecture数据集，已衍生出若干经典研究工作，例如基于GPT-5.4的自动证明尝试框架及其在Lean中的形式化实现。这些工作不仅展示了大型语言模型在数学推理中的潜力，还促进了计算证明与交互式定理证明工具的融合。此外，针对猜想趣味性与可解性的评估模型也为后续的智能数学助手系统奠定了方法论基础，引领了人工智能与数学交叉研究的新方向。