site.btaINSAIT and ETH Zurich Present Most Extensive Study of AI-Generated Mathematical Proofs

The Institute for Computer Science, Artificial Intelligence and Technology (INSAIT) at Sofia University and ETH Zurich presented the most extensive study to date of mathematical proofs generated by artificial intelligence, according to Sofia University’s press centre. The study covers the Open Proof Corpus (OPC), the largest corpus of mathematical proofs annotated by experts from INSAIT and ETH Zurich.

Proofcorpus.ai is a natural extension of the MathArena.ai platform, whose results have already been used by leading technology companies to create thinking models.

The goal of the next generation of AI is not only to give correct answers, but to create correct and well-founded proofs, Sofia University said in a press release.

OPC contains over 5,000 solutions generated by leading AI models such as Gemini 2.5 pro, OpenAI O3, OpenAI O4-mini, Qwen and DeepSeek R1. The problems are selected from 20 types of elite competitions, including the International Mathematical Olympiad (IMO). Each proof is labelled by human experts for correctness.

The study shows that thinking AI models are already approaching experts in evaluating proofs in terms of accuracy, but creating formal proofs remains a challenge for AI systems.