Advancing Mathematics Research with AI-Driven Formal Proof Search
This paper evaluates LLM-driven formal proof search on open mathematical problems, using Lean-style formal verification as the reliability layer for generat...
Soohak: A Mathematician-Curated Benchmark for Evaluating Research-level Math Capabilities of LLMs
这篇论文补的是 AI for math 评测中的关键缺口：很多数学 benchmark 更像竞赛题或形式化题库，而不是研究数学家实际会遇到的问题结构。Soohak 强调 mathematician-curated 和 research-level。 它的重要性在于让模型能力评估更接近真实数学研究：理解问题背景、...
AI Co-Mathematician: Accelerating Mathematicians with Agentic AI
这篇论文把数学 AI 从单题求解推进到 mathematician-facing agentic workflow。它关注的是如何协助数学家推进研究，而不是只在形式化证明 benchmark 上提高一点通过率。 这种 framing 对本库重要，因为 AI for math 的真正变化可能来自研究协作界面：提出...
DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
这篇论文抓住了 theorem-proving agent 的一个长期瓶颈：证明过程中产生的中间结果往往是一次性的，既不稳定，也不容易沉淀成跨题目可复用的知识资产。DreamProver 用 wake-sleep 循环把这个问题转成 lemma library 的持续演化。 它的价值不在某个 benchmark...
A prospective clinical feasibility study of a conversational diagnostic AI in an ambulatory primary care clinic
问题与背景：面向患者的对话式诊断 AI 在模拟环境中已有不少结果，但真正的临床转化难点在于：在真实就诊流程中，它是否安全、是否被患者和医生接受、以及它给出的诊断与管理建议是否具有实际价值。论文要回答的是这类系统能否跨出“模拟 benchmark”，进入真实门诊。 方法/新意：作者报告了一项前瞻性、单臂、真实世界...
Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design
**问题与背景** 这篇论文围绕 mathematical discovery / agentic systems / neurosymbolic methods 展开，目标是解决该方向里已经明确存在、但仍未被主流方法稳定解决的核心问题。按当前仓库标准，它属于值得正式收录的新作，因为问题本身有持续研究价值，且不...
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
- 分级：`突破性` - 正式标题：`LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics` - 原文：`2026-02-27-M2_LemmaBench-LemmaBench_A_Liv...
Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4
- 分级：`颠覆性` - 正式标题：`Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4` - 原文：`2026-02-09-M3_AutoReal_seL4-Towards_Real_Worl...
Semantic Search over 9 Million Mathematical Theorems
- 分级：`突破性` - 原文：`2026-02-05-M1_TheoremSearch_9_2M-Semantic_Search_over_9_Million_Mathematical_Theorems.pdf` - 抽取：`extracted.md` ## 重写摘要 这篇工作试图解决数学研究和自动证明里的一...
Not Quite Anything: Overcoming SAMs Limitations for 3D Medical Imaging
这篇论文讨论通用分割基础模型在 3D 医学影像上的失配问题。SAM/SAM-2 在自然图像上很强，但在脑 MRI 这类低对比、边界模糊的 3D 医学场景里效果明显下降。论文想解决的不是再训练一个更大的专用模型，而是如何让现有 foundation segmentation 模型真正适配 3D 医学图像。 方法上...
SoC-DT: Standard-of-Care Aligned Digital Twins for Patient-Specific Tumor Dynamics
这篇论文面向肿瘤动力学预测，关注在真实标准治疗流程下如何构建患者特异性的数字孪生。相比只做自然生长模拟的反应扩散模型，它把手术、放疗、化疗等标准治疗干预和基因组、人口统计学信息统一纳入一个可微分框架，用于预测治疗后的肿瘤结构演化。 方法上，论文提出 SoC-DT，把连续的肿瘤生长动力学与离散的标准治疗事件统一到...