Characterizing Initial Human-AI Proof Formalization Workflows

• Field: Machine Learning
• Authors: Katherine M. Collins, Simon Frieder, Jonas Bayer
• Date: 2025-06-01
• arXiv: 2506.00629

Summary

For centuries, human mathematicians have written proofs to substantiate their mathematical arguments; yet, the ability to automatically verify the validity of proofs has long been a challenge. Advances in AI systems' ability to generate code and engage in increasingly high-level mathematical reasoning promise to transform people's ability to formalize and thereby verify proofs. While many works focus on benchmarking the current frontier, this paper instead studies how people use these tools.

The authors conduct a mixed-methods analysis of the initial impact of AI on people's formalization workflows: what people claim they want, what they see as barriers to those visions, and how they actually use and adapt AI in practice.

Key findings

• A qualitative survey shows that people's preferences are diverse, but generally they want AI to assist in formalization while retaining high-level human control over the proof discovery process.
• A controlled user study asked participants to formalize informal mathematical problems and their proofs, comparing with-AI and without-AI conditions across problems of varying difficulty and mathematical domains.
• Despite the then-current limitations of automated formalization tools, participants allowed to use AI tools tended to achieve higher formalization accuracy.
• Most participants flexibly used multiple different AI tools during formalization.
• Overall, the work reveals the early stage of AI integration into formalization workflows, involving closely interleaved human-AI interaction.