Introduces AIM, a large-reasoning-model agent framework for frontier mathematical research, combining longer exploration trajectories with verification-oriented mechanisms for research-level proof tasks.
Publications
Papers and preprints from the AIM team.
Presents a human-AI co-discovery case study in which AIM-supported exploration, theorem formation, derivation, and audit workflows contributed to sign-embedding quantum algorithms for matrix equations and matrix functions.
Studies pessimistic verification workflows for open-ended mathematical proofs, where a proof is rejected when any verifier finds a critical error.
Presents a homogenization-theory case study showing how AIM-assisted reasoning and targeted human intervention can support the development of a complete mathematical proof.
Proposes FormaRL, a reinforcement-learning framework for autoformalization that uses unlabeled data, Lean syntax checks, and LLM consistency checks to improve formalization accuracy.