This talk provides an overview of NeuroSymbolic AI research at the intersection of large language models and the Lean theorem prover, exploring two complementary directions that demonstrate the symbiotic relationship between AI and formal systems. We examine how LLMs can enhance proof automation and user experience in formal mathematics by analyzing theorem statements and proof contexts to suggest relevant tactics and identify common mistakes, while also showing how Lean-derived datasets can improve models’ reasoning capabilities across diverse domains including mathematics, coding, and planning. We apply Reinforcement Learning with Verifiable Reward (RLVR) where Lean serves as the verifier, enabling models to generate complete formal proofs that are validated through Lean’s verification system rather than just checking boxed answers. We also highlight two challenging problems deserving community attention: (i) proof optimization for improving training efficiency and (ii) proof modernization for leveraging evolving Lean ecosystems.

Speaker Bio: Soonho Kong is a Principal Applied Scientist for Amazon Web Services within the NeuroSymbolic AI Lab. His research focuses on designing and implementing AI systems with formal reasoning capabilities, particularly combining LLMs with interactive and automated theorem proving techniques. His work helps improve Amazon Nova models with advanced reasoning capabilities. He earned his PhD from Carnegie Mellon University under Prof. Edmund Clarke, focusing on delta-decision procedures. He received the CADE Skolem Award for his contributions to the Lean theorem prover.