Robert Joseph George - Building Trustworthy AI for Mathematics and Science
Discussion description: AI systems are becoming increasingly capable at mathematics, coding, and scientific reasoning, but generating a convincing answer is very different from generating one that can be rigorously trusted. In this discussion, I’ll begin with a brief introduction to Lean and formal theorem proving, and explain how formal methods can be used to make mathematical and computational reasoning machine-checkable. I’ll then discuss our work on TorchLean, a framework for verified machine learning in Lean, including neural-network execution, automatic differentiation, floating-point s