# Human agency in initial human-AI proof formalization workflows

arXiv: https://arxiv.org/abs/2606.04273 · HTML: https://mlsanity.com/paper/2606.04273/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 35 of its 72 references that are in the map.
- First posted on arXiv 2 Jun 2026.

## Builds on (most cited first, 30 of 35)

- [OpenHands: An Open Platform for AI Software Developers as Generalist Agents](https://mlsanity.com/paper/2407.16741/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [The Impact of AI on Developer Productivity: Evidence from GitHub Copilot](https://mlsanity.com/paper/2302.06590/) (2023)
- [Using an LLM to Help With Code Understanding](https://mlsanity.com/paper/2307.08177/) (2023)
- [Grounded Copilot: How Programmers Interact with Code-Generating Models](https://mlsanity.com/paper/2206.15000/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity](https://mlsanity.com/paper/2507.09089/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Productivity Assessment of Neural Code Completion](https://mlsanity.com/paper/2205.06537/) (2022)
- [The Programmer's Assistant: Conversational Interaction with a Large Language Model for Software Development](https://mlsanity.com/paper/2302.07080/) (2023)
- [Reading Between the Lines: Modeling User Behavior and Costs in AI-Assisted Programming](https://mlsanity.com/paper/2210.14306/) (2022)
- [Studying the effect of AI Code Generators on Supporting Novice Learners in Introductory Programming](https://mlsanity.com/paper/2302.07427/) (2023)
- ["It's Weird That it Knows What I Want": Usability and Interactions with Copilot for Novice Programmers](https://mlsanity.com/paper/2304.02491/) (2023)
- [Rapid trial-and-error learning with simulation supports flexible tool use and physical reasoning](https://mlsanity.com/paper/1907.09620/) (2019)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [The RealHumanEval: Evaluating Large Language Models' Abilities to Support Programmers](https://mlsanity.com/paper/2404.02806/) (2024)
- [Code with Me or for Me? How Increasing AI Automation Transforms Developer Workflows](https://mlsanity.com/paper/2507.08149/) (2025)
- [How Do Analysts Understand and Verify AI-Assisted Data Analyses?](https://mlsanity.com/paper/2309.10947/) (2023)
- [Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions](https://mlsanity.com/paper/2302.07248/) (2023)
- [Examining the Use and Impact of an AI Code Assistant on Developer Productivity and Experience in the Enterprise](https://mlsanity.com/paper/2412.06603/) (2024)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning](https://mlsanity.com/paper/2412.15184/) (2024)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Generative Modeling for Mathematical Discovery](https://mlsanity.com/paper/2503.11061/) (2025)
- [Abstraction boundaries and spec driven development in pure mathematics](https://mlsanity.com/paper/2309.14870/) (2023)

## Abstract (arXiv)

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, we instead study how people use these tools and apply agency in doing so. We conduct a mixed-methods analysis into the initial impact of AI on people's formalization workflows: what people claim they want, what they see as the barriers to those visions, and how they actually use and adapt AI in practice. A qualitative survey reveals that people's preferences are diverse, but with a general desire for AI assistance in formalization that preserves high-level human control and agency over the proof discovery process. To assess how people actually engage with AI for formalization, we conduct a controlled user study in which participants formalize informal math problems and their proofs, with and without AI, across a range of mathematical problems at varying levels of difficulty and domains. Despite limitations of the tools at the time for autoformalization, participants tended to attain higher formalization accuracy when allowed access to AI tools than when formalizing on their own, with most participants flexibly choosing to use multiple different AI tools. Taken together, our work sheds light on the early stages of AI integration into formalization workflows, involving an intimate interplay of human agency and AI engagement.