This paper investigates how AI agents behave differently from human collaborators in the interactive theorem‑proving environment Lean. The authors introduce a "simulated collaboration" methodology that records AI and human actions side‑by‑side across nine major human projects (4.7 M definitions, over 6 K commits) to address two questions: (1) whether AI focuses more on surface syntax or deeper semantics, and (2) where AI’s next‑step preferences diverge from those of humans.\nThe study reveals three consistent tendencies as proofs evolve:\n- AI agents are far more attracted to explicitly marked gaps than humans;\n- they avoid densely connected proof centers and complex or surprising goals;\n- they show curiosity toward surprising proof bodies but tend to regularize them toward baseline patterns.\nThese findings highlight blind spots in human‑AI mathematical collaboration and suggest interventions such as encouraging semantic awareness and reducing reliance on superficial markers to improve joint productivity.\n\nReview: The work offers a rigorous experimental framework that clarifies the divergent reasoning patterns of AI and humans in proof formalization, providing valuable insights for designing more effective collaborative tools.