Bolzano's authors report about 200 solutions among 3,800 open problems

Eight researchers at Charles University, one of them also at the Czech Academy of Sciences, have posted a paper on a multi-agent system they call Bolzano. arXiv:2610.09769, “From Expert-Guided Proof Search to Automated Open-Problem Solving,” was submitted on 7 October 2026. The comments field, and a line in the PDF, say it was accepted at the 6th Workshop on Mathematical Reasoning and AI (MATH-AI) at NeurIPS 2026. A workshop acceptance is not a journal publication.

The authors are Adrián Zámečník, Matěj Kripner, Martin Koutecký, Martin Balko, Jan Grebík, Pavel Hubáček, Robert Šámal and Václav Rozhoň. The PDF lists the Computer Science Institute, the Institute of Formal and Applied Linguistics, and the Department of Applied Mathematics, all at Charles University, and the Institute of Mathematics of the Czech Academy of Sciences. Hubáček carries both the computer science institute and the academy.

What the system does

The abstract says Bolzano uses parallel prover agents, a verifier agent, and a human-readable research state. An agent, in the paper, is one model call with a role-specific prompt and the notes it is given. Each round, provers see the same documents and work at the same time, without seeing one another’s answers for that round. Only the verifier may update the shared files: notes, candidate proofs, and an outcome page. A summarizer writes a short account for the next round. In the reported runs those three roles had no web search, no code execution and no other tools. The verifier is another language model. The paper says an incorrect lemma can sit in that memory and be repeated later, so the documents stay candidate mathematics until a person or a formal system checks them.

Table 1 names the models. New arXiv papers and the STOC 2026 set used GPT-5.5 for four rounds. Earlier FOCS, SODA and STOC papers, and the Midsummer Combinatorial Workshop set, used GPT-5.6 Sol for two rounds. Each run used one prover.

What “solved” means in the table

The abstract says manual use on expert-selected problems produced 8 results whose proofs were checked by domain experts. It then says unguided runs on about 3,800 open problems from four sets of papers solved about 200. Table 1 breaks that down: 1,600 problems from new arXiv papers in combinatorics and data structures (90 solved), 420 from STOC 2026 (4 solved), 900 from earlier FOCS, SODA and STOC papers (40 solved), and 880 from the Midsummer Combinatorial Workshop (80 solved). The solved column sums to 214, and 485 outputs were flagged as promising.

A footnote defines the solved counts. Except for STOC 2026, they are estimates, partly from model assessments of whether the output addresses the question and whether the argument is substantially correct. The authors say feedback from source-paper authors on many results makes those estimates reasonable. For STOC 2026 they report only four results they checked and that the source papers’ authors verified. Those authors, the paper says, confirmed the results in private correspondence in June and July 2026. A further footnote says that for two of the four, convex quartics and biased CAT states, the authors reviewed the main idea and not the full proof.

The four STOC items, as the paper states them, are a low-memory test for a planted biclique, a separation between two kinds of monotone programs, a convex quartic with a single irrational witness, and a circuit-depth bound for biased CAT states, including a case the source paper had left open.

How to read the number

About 200 of about 3,800 is the abstract’s round number for Table 1’s 214. The human-checked slice is the 8 expert-checked results plus 4 STOC answers, two of those confirmed on the main idea alone. The rest of the solved column is an estimate, and the in-loop verifier is a model. OpenAI’s manuscript release is a different corpus with the same caution: a write-up still needs a check.