Minghao Pan

Chenyang An, Qihao Ye, Minghao Pan et al.

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.

Manuel Mueller-Frank, Minghao Pan, Omer Tamuz

The value of proof-of-work cryptocurrencies critically depends on miners having incentives to follow the protocol. However, the Bitcoin mining protocol proposed by Nakamoto (2008) and implemented in practice is well known not to constitute an equilibrium: Eyal and Sirer (2018) construct a profitable deviation called ``selfish mining'' which relies on strategically delaying disclosure of newly mined blocks rather than publishing them immediately. We propose inertial mining, a novel mining protocol. When miners follow inertial mining, they produce the outcome intended by Nakamoto, i.e., a single longest chain. But unlike the Bitcoin mining protocol, inertial mining constitutes an equilibrium (assuming no miner controls more than half of the mining power). Indeed, neither selfish mining nor any other deviation is profitable. Furthermore, inertial mining only changes miners' behavior in the event of off-path forks, and can be implemented in Bitcoin without any changes to its consensus mechanism or blockchain architecture.