Zhi-Jian Lai

A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

This work proposes a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs, which retains control over problem formulation and assumptions, while the model searches for proofs or contradictions, proposes candidate properties and theorems, and helps construct structures and parameters that s...