Characterizing initial human-AI proof formalization workflows

• URL: http://arxiv.org/abs/2606.04273v1
• Date: Tue, 02 Jun 2026 22:58:19 GMT
• Title: Characterizing initial human-AI proof formalization workflows
• Abstract summary: 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.<n>We conduct a mixed-methods analysis into the initial impact of AI on people's formalization.<n>A qualitative survey shows that people's preferences are diverse, but with a general desire for AI assistance in formalization.
• Score: 66.06866890889131
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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. 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 shows that people's preferences are diverse, but with a general desire for AI assistance in formalization that preserves high-level human control over the proof discovery process. To assess how people actually engage with AI for formalization under such limitations, 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 tend 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 and AI engagement.

Related papers

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• AI usage patterns are shaped by perceived gains in human agency [2.2635515032445577]
  We show that people consistently link sustained AI usage to perceived gains in individual agency.<n>Our findings challenge prevailing assumptions about how and why humans use AI systems over time.
  arXiv  Detail & Related papers  (2026-07-02T15:24:58Z)
• AI Phenomenology for Understanding Human-AI Experiences Across Eras [8.54750896635797]
  We argue for AI phenomenology: a research stance that asks "How did it feel?" when interacting with AI systems.<n>We motivate AI phenomenology as a framework that captures how alignment is experienced, negotiated, and updated between users and AI systems.
  arXiv  Detail & Related papers  (2026-03-09T23:26:46Z)
• The AI Research Assistant: Promise, Peril, and a Proof of Concept [0.0]
  We provide empirical evidence through a detailed case study.<n>The collaboration revealed both remarkable capabilities and critical limitations.<n>Our experience suggests that, when used with appropriate skepticism and verification protocols, AI tools can meaningfully accelerate mathematical discovery.
  arXiv  Detail & Related papers  (2026-02-26T10:29:05Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  We introduce Aletheia, a math research agent that iteratively generates, verifies, and revises solutions end-to-end in natural language.<n>Specifically, Aletheia is powered by an advanced version of Gemini Deep Think for challenging reasoning problems.<n>We demonstrate Aletheia from Olympiad problems to PhD-level exercises and most notably, through several distinct milestones in AI-assisted mathematics research.
  arXiv  Detail & Related papers  (2026-02-10T18:50:15Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  We advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level.<n>We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
  arXiv  Detail & Related papers  (2024-12-20T17:19:24Z)
• Improving Human-AI Collaboration With Descriptions of AI Behavior [14.904401331154062]
  People work with AI systems to improve their decision making, but often under- or over-rely on AI predictions and perform worse than they would have unassisted. To help people appropriately rely on AI aids, we propose showing them behavior descriptions.
  arXiv  Detail & Related papers  (2023-01-06T00:33:08Z)
• On the Effect of Information Asymmetry in Human-AI Teams [0.0]
  We focus on the existence of complementarity potential between humans and AI. Specifically, we identify information asymmetry as an essential source of complementarity potential. By conducting an online experiment, we demonstrate that humans can use such contextual information to adjust the AI's decision.
  arXiv  Detail & Related papers  (2022-05-03T13:02:50Z)
• Cybertrust: From Explainable to Actionable and Interpretable AI (AI2) [58.981120701284816]
  Actionable and Interpretable AI (AI2) will incorporate explicit quantifications and visualizations of user confidence in AI recommendations. It will allow examining and testing of AI system predictions to establish a basis for trust in the systems' decision making.
  arXiv  Detail & Related papers  (2022-01-26T18:53:09Z)
• A User-Centred Framework for Explainable Artificial Intelligence in Human-Robot Interaction [70.11080854486953]
  We propose a user-centred framework for XAI that focuses on its social-interactive aspect. The framework aims to provide a structure for interactive XAI solutions thought for non-expert users.
  arXiv  Detail & Related papers  (2021-09-27T09:56:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.