何世紀にもわたり、数学者は数学的議論を実証するために証明を記述してきたが、証明の妥当性を自動的に検証する能力は長きにわたり課題であった。AIシステムのコード生成能力と高度な数学的推論能力の進歩は、人々が証明を形式化し、それによって検証する能力を変革する可能性を秘めている。多くの研究は現在のフロンティアのベンチマークに焦点を当てているが、本論文は代わりに人々がこれらのツールをどのように使用しているかを研究する。著者らは、AIが形式化ワークフローに及ぼす初期の影響について混合手法分析を行い、人々が何を望んでいると主張しているか、そのビジョンへの障壁をどのように見ているか、そして実際にAIをどのように使用し適応させているかを調査した。
定性調査によると、人々の選好は多様であるが、形式化におけるAI支援を求めつつ、証明発見プロセスに対する高水準の人間の制御を維持したいという一般的な願望があることが示された。このような制限の下で人々が実際にどのようにAIと関わるかを評価するため、研究者らは制御されたユーザー研究を実施した。参加者は、さまざまな難易度と領域の非公式な数学問題とその証明を、AIの有無にかかわらず形式化した。
当時の自動形式化ツールの限界にもかかわらず、参加者はAIツールへのアクセスが許可された場合、単独で形式化する場合よりも高い形式化精度を達成する傾向があった。大多数の参加者は、複数の異なるAIツールを柔軟に選択して使用した。総じて、この研究は、人間とAIの緊密な相互作用を含む形式化ワークフローへのAI統合の初期段階を明らかにするものである。
本論文はKatherine M. Collinsら17名の著者によって執筆され、2026年6月2日にarXivに提出された。人工知能（cs.AI）分野に属し、arXiv識別子は2606.04273である。研究は、形式化プロセスにおける人間の制御とAI支援のバランスを強調し、将来のツール設計に対する実証的根拠を提供する。