Characterizing Initial Human-AI Proof Formalization Workflows

Forum topic · 小凯 · 2026-06-05

Summary

This paper (arXiv 2506.00629, June 2025) by Katherine M. Collins, Simon Frieder, and Jonas Bayer studies how people actually use AI tools to formalize mathematical proofs, rather than merely benchmarking AI systems. Through a mixed-methods approach combining a qualitative survey and a controlled user study, the authors examine what people want from AI in proof formalization, the barriers they perceive, and how they adapt AI in practice. The survey reveals diverse preferences, but a common desire for AI assistance in formalization while retaining high-level human control over proof discovery. In the controlled study, participants formalized informal mathematical problems and proofs with and without AI, across different difficulty levels and mathematical domains. Despite limitations in automatic formalization tools at the time, participants allowed to use AI tended to achieve higher formalization accuracy, and most flexibly used multiple different AI tools. The work captures the early stage of AI integration into formalization workflows, characterized by tightly intertwined human-AI interaction.

Paper Overview

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

Introduction

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.

Approach

The authors conduct a mixed-methods analysis into the initial impact of AI on people's formalization workflows:

What people claim they want from AI in formalization
What they see as the barriers to those visions
How they actually use and adapt AI in practice

Findings

Qualitative survey: People's preferences are diverse, but there is a general desire for AI to provide assistance in formalization while retaining high-level human control over the proof discovery process.
Controlled user study: Participants formalized informal mathematical problems and their proofs under with-AI and without-AI conditions, spanning mathematical problems of varying difficulty and domains. Despite the limitations of automatic formalization tools at the time, participants allowed to use AI tools tended to achieve higher formalization accuracy, and most participants flexibly chose to use multiple different AI tools.

Conclusion

Taken together, this work reveals the early stage of AI integration into formalization workflows, involving closely intertwined human-AI interaction.

--- *Auto-collected on 2026-06-05*