Human–AI Collaboration in Mathematics: A Practical Account

Human–AI collaboration in mathematics decouples the development of an argument with the construction of its formal derivation. In our approach, the researcher maintains a dependency-ordered graph of definitions, hypotheses, constructions, and intermediate claims; the agent develops proofs and asks where an argument is incomplete or a connecting step is absent. Answering those questions can require new mathematics, a different construction, or a revision of the question itself. This practice grew from examining an unattended attempt at ten research-mathematics problems and supported a three-week Lean development in learning theory. Ghost-sample symmetrization, confidence boosting, compression, and measurability constructions required sustained mathematical direction across connected proofs. The resulting specification separates review of mathematical commitments from checking their derivations, preserves unresolved extensions, and reopens affected decisions when premises change. An open-source adaptation of DeepSeek Harness makes these responsibilities executable. This division of work let me direct substantial mathematical construction while retaining authorship of the arguments that determined what we established.