Xiangdong Ye

works on

formal verification 1 human-in-the-loop 1 interactive theorem proving 1 large language models 1 Lean4 1

From the 1 of 3 linked papers with an AI index.

collaborators

3 papers

cs.AI2026

MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

Junjie Zhang, Jiayu Liu, Wenbin Liu +11

MathCoPilot is an interactive, human‑in‑the‑loop system that lets mathematicians steer AI agents to formalize and verify mathematical proofs in Lean, combining a live proof bluepri…

math.NT2026

Mod $ℓ$ non-vanishing of self-dual Hecke $L$ -values over CM fields and applications

Ashay Burungale, Wei He, Ye Tian +1

Let $I^»$ be a self-dual Hecke character over a CM field $K$ . Let $p$ be a degree one prime of the maximal totally real subfield $F$ of $K$ and $I^_{p}$ the Ga…

math.DS2025

On systems disjoint from all minimal systems

Wen Huang, Song Shao, Hui Xu +1

Recently, GÃ³rska, LemaÅczyk, and de la Rue characterized the class of automorphisms disjoint from all ergodic automorphisms. Inspired by their work, we provide several characteri…

MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

Mod ℓ non-vanishing of self-dual Hecke L-values over CM fields and applications

On systems disjoint from all minimal systems

Mod $ℓ$ non-vanishing of self-dual Hecke $L$ -values over CM fields and applications