Project Grant 2617441

The National Science Foundation Division of Mathematical Sciences awarded the University of California, Los Angeles $1.08 million on September 1, 2026, under the Mathematical and Physical Sciences program (CFDA 47.049) to develop a human-centered, AI-assisted framework for interactive mathematical reasoning and discovery.

The project, running through August 31, 2029, establishes effective human-AI collaboration paradigms that adapt to user expertise while preserving interpretability and mathematical intent. UCLA will build robust mathematical reasoning models through curriculum learning and contrastive learning, using high-quality, research-aligned synthetic data generation to capture the diversity of proof styles and definition systems employed by mathematicians. The work includes developing interactive reasoning tools using formal theorem proving as a demanding use case that supports both exploration and verification through structured knowledge representations. Key innovations encompass adaptive collaboration interfaces that modulate AI assistance according to user expertise, an integrated human-AI data generation workflow producing high-fidelity training data through controllable blueprint construction and robustness testing of definitions, and an interactive theorem prover capable of reliably following human guidance via structured constraints. Performance occurs in Los Angeles, California.