Yiming Fu

Yiming Fu, Peixuan Liu, Zichen Wang et al.

While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries. We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines, which encourages monolithic or ad hoc proof scripts rather than library-quality artifacts. Existing approaches to proof-quality improvement often rely on explicit, computable optimization objectives. In practice, however, the most tractable and experimentally validated objectives are largely length-based, while higher-level qualities such as readability, modularity, maintainability, and reusability are difficult to reduce to reliable automatic metrics. Instead of optimizing proof improvement against a single proxy metric, we take a process-guided approach inspired by human proof-refactoring workflows. We propose an agentic framework $\textbf{Proof-Refactor}$ that decomposes proof refactoring into four phases: extracting candidate proof fragments, designing helper declarations, formally proving the extracted and designed components, and repairing the original proof using the verified components. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves rubric-based refactoring scores over a strong Claude Code refactoring baseline, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve proof structure without treating proof length as the primary objective.

Rongge Xu, Hui Dai, Yiming Fu et al.

While large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, current benchmarks fail to adequately measure library-grounded abstraction -- the ability to reason with high-level interfaces and reusable structures central to modern mathematics and software engineering. We introduce LeanCat, a challenging benchmark comprising 100 fully formalized category-theory tasks in Lean. Unlike algebra or arithmetic, category theory serves as a rigorous stress test for structural, interface-level reasoning. Our evaluation reveals a severe abstraction gap: the best state-of-the-art model solves only 12.0% of tasks at pass@4, with performance collapsing from 55.0% on Easy tasks to 0.0% on High-difficulty tasks, highlighting a failure in compositional generalization. To overcome this, we evaluate LeanBridge, a retrieval-augmented agent that employs a retrieve-generate-verify loop. LeanBridge achieves a peak success rate of 24.0% -- doubling the performance of the best static baseline. These results empirically demonstrate that iterative refinement and dynamic library retrieval are not merely optimizations but strict necessities for neuro-symbolic reasoning in abstract domains. LeanCat offers a compact, reusable testbed for tracking progress toward reliable, research-level formalization.

Yu Mei, Xutong Wang, Ziyao Zhang et al.

Emotion education is critical for children aged 3 to 6. However, existing technologies largely focus on children's direct interaction with AI, overlooking the central role of parents in guiding early emotional development at home. To address this gap, we conducted co-design sessions with five kindergarten teachers and five parents to identify key parental challenges and opportunities for AI support in family emotion education. Based on these insights, we developed PACEE, an LLM-based assistant designed to support parents in guiding children's emotional development through conversations, rather than directly interacting with children. PACEE provides parent-centered AI scaffolding that supports parents in real-time conversation through personalized guidance, post-hoc reflection through trackable feedback, and understanding children's emotional states through modeling. We evaluated PACEE with 16 families. Results show that PACEE enhances parent-child engagement, fosters deeper emotional communication, and improves parents' expertise and overall experience in guiding their children. Our findings extend emotion coaching practices to the context of generative AI and offer design insights for building AI systems that support parent-centered family education.