may 22, 2026
AI for Science: AI as a Mathematician
Przemek Chojecki and our own Bartosz Naskręcki led an AI for Science session at the Centre on formal proofs, proof assistants, and the role of AI systems in mathematical practice.
may 22, 2026
AI for Science: AI as a Mathematician
Przemek Chojecki and our own Bartosz Naskręcki led an AI for Science session at the Centre on formal proofs, proof assistants, and the role of AI systems in mathematical practice.
On 22 May 2026, the Centre for Credible AI hosted AI as a Mathematician, a session in the AI for Science series, at Rektorska 4 in Warsaw. The session was led by Przemek Chojecki of ulam.ai and by our own Bartosz Naskręcki, a researcher at the Centre for Credible AI and at Adam Mickiewicz University in Poznań.
The talks covered what counts as a proof once a machine has to check it, the interactive proof assistants that make this possible, and the ways machine learning and formal methods are converging on the same problems. The speakers closed with a case study of a workflow combining human and machine work.
Questions from the Discussion
Most of the session was given over to discussion. Recurring questions included:
- Will mathematicians focus mainly on proposing hypotheses and conjectures, with verification delegated to AI systems?
- If an AI-generated proof is formally correct, does understanding it still matter?
- Will the role of the mathematician shift from constructing proofs towards interpreting and validating reasoning produced by AI?
- Can AI models generate genuinely new mathematical theories?
- What is mathematics in the era of advanced AI systems, and do proofs that remain inaccessible to human comprehension provide limited scientific value?
Our thanks to Przemek Chojecki and Bartosz Naskręcki for leading the session, and to everyone who took part in the discussion. The next AI for Science meeting is in preparation.