AI Impact on Human Proof Formalization Workflows

Human mathematicians have written proofs for centuries to substantiate their mathematical arguments. The ability to automatically check the validity of proofs has long been a dream. The development of tools for such checking of "formalized" proofs has been made possible by new languages for formal mathematics, like Lean. Advances in AI systems' ability to generate code promises to transform the ability to formalize proofs and to assist humans in this task. Recent studies have examined how human programmers engage with AI tools for code generation, but the role of AI in humans' formalization process is comparatively understudied. Here, we conduct an initial exploration into people's formalization process with and without AI. We collect more than 80 hours of video from seven participants formalizing informal proofs with and without AI on a range of mathematical problems covering different levels of difficulty and domains. We offer a first characterization of people's formalization process, noting places where AI assistance helps --- and a few instances where it may hurt.