Daily Papers

We explore a central question in AI for mathematics: can AI systems produce original, nontrivial proofs for open research problems? Despite strong benchmark performance, producing genuinely novel proofs remains an outstanding challenge for LLMs. Through systematic experiments with frontier LLMs on research-level proof tasks, we identify seven failure modes that prevent reliable proof generation, including context contamination, citation hallucination, hand-waving on key steps and misallocation of proof effort, unstable proof plans, unfocused verification, problem modification and single-model bottleneck. We argue that the gap between benchmark success and research-level proving is primarily one of system design, due to those failure modes. We present QED, an open-source multi-agent proof system in which each architectural decision directly addresses a specific failure mode. Evaluated on five open problems in applied analysis and PDEs contributed by domain experts, QED produces correct proofs for three problems, each verified by the contributing experts as original and nontrivial. QED is released as open-source software at https://github.com/proofQED/QED.

Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematical Olympiad (IMO). However, the training pipelines behind these systems remain largely undisclosed, and their reliance on large "internal" models and scaffolds makes them expensive to run, difficult to reproduce, and hard to study or improve upon. This raises a central question: can small, open models also be trained to achieve competitive reasoning performance on difficult Olympiad-level math? In this paper, we answer this question by building QED-Nano, a 4B model post-trained for Olympiad-level proofs. Our training recipe has three stages: (1) supervised fine-tuning to imbue good proof-writing styles by distilling from DeepSeek-Math-V2, (2) reinforcement learning (RL) with rubric-based rewards, and (3) expanding RL with a reasoning cache, which decomposes long proofs into iterative summarize-and-refine cycles and enables stronger test-time reasoning. QED-Nano surpasses the proof-generation performance of much larger open models, including Nomos-1 and GPT-OSS-120B, and approaches the performance of proprietary models like Gemini 3 Pro, at a fraction of the inference cost. To support further research on open mathematical reasoning, we release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.

A question answering system that in addition to providing an answer provides an explanation of the reasoning that leads to that answer has potential advantages in terms of debuggability, extensibility and trust. To this end, we propose QED, a linguistically informed, extensible framework for explanations in question answering. A QED explanation specifies the relationship between a question and answer according to formal semantic notions such as referential equality, sentencehood, and entailment. We describe and publicly release an expert-annotated dataset of QED explanations built upon a subset of the Google Natural Questions dataset, and report baseline models on two tasks -- post-hoc explanation generation given an answer, and joint question answering and explanation generation. In the joint setting, a promising result suggests that training on a relatively small amount of QED data can improve question answering. In addition to describing the formal, language-theoretic motivations for the QED approach, we describe a large user study showing that the presence of QED explanations significantly improves the ability of untrained raters to spot errors made by a strong neural QA baseline.

As Large Language Models (LLMs) saturate elementary benchmarks, the research frontier has shifted from generation to the reliability of automated evaluation. We demonstrate that standard "LLM-as-a-Judge" protocols suffer from a systematic Alignment Gap when applied to upper-undergraduate to early graduate level mathematics. To quantify this, we introduce QEDBench, the first large-scale dual-rubric alignment benchmark to systematically measure alignment with human experts on university-level math proofs by contrasting course-specific rubrics against expert common knowledge criteria. By deploying a dual-evaluation matrix (7 judges x 5 solvers) against 1,000+ hours of human evaluation, we reveal that certain frontier evaluators like Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, and Llama 4 Maverick exhibit significant positive bias (up to +0.18, +0.20, +0.30, +0.36 mean score inflation, respectively). Furthermore, we uncover a critical reasoning gap in the discrete domain: while Gemini 3.0 Pro achieves state-of-the-art performance (0.91 average human evaluation score), other reasoning models like GPT-5 Pro and Claude Sonnet 4.5 see their performance significantly degrade in discrete domains. Specifically, their average human evaluation scores drop to 0.72 and 0.63 in Discrete Math, and to 0.74 and 0.50 in Graph Theory. In addition to these research results, we also release QEDBench as a public benchmark for evaluating and improving AI judges. Our benchmark is publicly published at https://github.com/qqliu/Yale-QEDBench.

An infinite number of physically nontrivial symmetries are found for abelian gauge theories with massless charged particles. They are generated by large U(1) gauge transformations that asymptotically approach an arbitrary function varepsilon(z,z) on the conformal sphere at future null infinity (mathscr I^+) but are independent of the retarded time. The value of varepsilon at past null infinity (mathscr I^-) is determined from that on mathscr I^+ by the condition that it take the same value at either end of any light ray crossing Minkowski space. The varepsilonneq constant symmetries are spontaneously broken in the usual vacuum. The associated Goldstone modes are zero-momentum photons and comprise a U(1) boson living on the conformal sphere. The Ward identity associated with this asymptotic symmetry is shown to be the abelian soft photon theorem.

We study the S-matrix and inclusive cross-section for general dressed states in quantum electrodynamics. We obtain an infrared factorization formula of the S-matrix elements for general dressed states. It enables us to study what dressed states lead to infrared-safe S-matrix elements. The condition for dressed states can be interpreted as the memory effect which is nothing but the conservation law of the asymptotic symmetry. We derive the generalized soft photon theorem for general dressed states. We also compute inclusive cross-section using general dressed states. It is necessary to use appropriate initial and final dressed states to evaluate interference effects, which cannot be computed correctly by using Fock states due to the infrared divergence.

Quantum simulation of many-body systems in materials science and chemistry are promising application areas for quantum computers. However, the limited scale and coherence of near-term quantum processors pose a significant obstacle to realizing this potential. Here, we theoretically outline how a single-circuit quantum electrodynamics (cQED) device, consisting of a transmon qubit coupled to a long-lived cavity mode, can be used to simulate the ground state of a highly-entangled quantum many-body spin chain. We exploit recently developed methods for implementing quantum operations to sequentially build up a matrix product state (MPS) representation of a many-body state. This approach re-uses the transmon qubit to read out the state of each spin in the chain and exploits the large state space of the cavity as a quantum memory encoding inter-site correlations and entanglement. We show, through simulation, that analog (pulse-level) control schemes can accurately prepare a known MPS representation of a quantum critical spin chain in significantly less time than digital (gate-based) methods, thereby reducing the exposure to decoherence. We then explore this analog-control approach for the variational preparation of an unknown ground state. We demonstrate that the large state space of the cavity can be used to replace multiple qubits in a qubit-only architecture, and could therefore simplify the design of quantum processors for materials simulation. We explore the practical limitations of realistic noise and decoherence and discuss avenues for scaling this approach to more complex problems that challenge classical computational methods.