2 citations · 2 across the 4 of their papers we have counts for
4 papers
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Jialin Lu, Soonho Kong, Rodrigo Stehling +4
We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proo…
Lean Finder: Semantic Search for Mathlib That Understands User Intents
Jialin Lu, Kye Emond, Kaiyu Yang +3
We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hi…
PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs
Mauricio Soroco, Jialin Song, Mengzhou Xia +3
While recent AI-for-math has made strides in pure mathematics, areas of applied mathematics, particularly PDEs, remain underexplored despite their significant real-world applicatio…
Pickleball Flight Dynamics
Kye Emond, Weiran Sun, Tim B Swartz
This paper considers the flight dynamics of the ball in the sport of pickleball. Various simplifications are introduced according to the features of the game. These simplifications…