1. LLMs for Proof Generation and Verification

    How GPT-5.5 Pro generated a proof resolving the binary-matrix case of a 1997 conjecture—and why pairing LLM proof generation with Lean verification may become a common mathematical workflow.

    中文版