Open-source multi-agent system run unattended on about 3,800 open problems from research papers; about 200 reported solved, four STOC 2026 questions confirmed by the papers’ authors

Your AI and this story

Key facts

• Paper: ‘Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving’, arXiv 2610.09769 [cs.AI], 7 Oct 2026 (v2 9 Oct); ‘Accepted at the 6th Workshop on Mathematical Reasoning and AI (MATH-AI), NeurIPS 2026’
• Table 1 (problems / model / rounds / promising / solved): arXiv math.CO and cs.DS 1,600 / GPT-5.5 / 4 / 250 / 90; STOC 2026 420 / GPT-5.5 / 4 / 41 / 4; earlier FOCS, SODA and STOC 900 / GPT-5.6 Sol / 2 / 57 / 40; Midsummer Combinatorial Workshop 880 / GPT-5.6 Sol / 2 / 137 / 80; total 3,800 / 485 / 214
• Caveat (Table 1 footnote): ‘Except for STOC 2026, the solved counts are estimates. These estimates are partially informed by LLM-based assessments of whether the output addresses the source question and whether its argument is substantially correct.’ For STOC 2026 only the four results checked by the team and verified by the source papers’ authors are counted
• Setup: ‘the prover, verifier, and summarizer operated without web search, code execution, direct filesystem access, or any tools’; all runs used one prover at the maximum reasoning effort; open problems were extracted from the papers by a separate LLM workflow with literature search
• STOC 2026 results, confirmed ‘in private correspondence in June and July 2026’: a one-pass O(log n)-memory algorithm detecting a semi-random planted biclique with sides at least Cn^(2/3) (question from Garg, Hastings, Pabbaraju and Sharan); an exponential separation between monotone rank programs and monotone span programs (Cavalar et al.); a strongly convex rational quartic in two variables whose zero sublevel set is a single irrational point (Slot, Steurer and Wiedmer); an Ω(log n) circuit-depth lower bound for joining and splitting biased CAT states (Parham)
• Footnote: for the convex-quartic and CAT-state results ‘the authors reviewed only the main idea, not the full proof’
• Paper: ‘Bolzano found a few hundred solutions, which we sent to authors of the source papers, some of whom plan to include these results in revised versions of their papers.’
• Limits stated by the authors: ‘The verifier is another LLM, not a formal proof checker. An accepted but incorrect lemma may propagate through persistent memory’; observed failures ‘include missing assumptions, proofs addressing weaker versions of the original questions, invalid arguments and rediscoveries of known results’; there is ‘no comparison with direct use of the underlying models’