Events
Department of Mathematics and Statistics
Texas Tech University
In the AI era, most people ask mathematics questions to AI, from kindergarten to PhD level. The problem is: are those answers trustworthy? How does the AI come up with those solutions? Unfortunately, most of the time, the mathematical proofs produced by AI are either hallucinated, lack rigor, or contain incorrect steps. So how do we train a machine to give precise proofs? In this talk, we address this problem from a differential geometry perspective using Lean. Lean plays a very different role among computer programming languages compared to Python, Mathematica, MATLAB, or any other computer-aided systems. All the aforementioned languages are capable of solving numerical and symbolic problems in a very systematic way. However, Lean is different: it is designed for writing formally verified mathematical proofs and creating verified software. Using Lean gives the machine a precise proof and provides insight into how the machine understands your findings. Moreover, it minimizes human errors. In this talk, we begin with an introduction to Lean and the paradigm of formal proof verification, highlighting why proof assistants are gaining adoption in contemporary mathematics. We present some simple examples in differential geometry and then survey the current state of differential geometry in Lean’s mathematical library (Mathlib), examining what has been formalized and what remains open. This talk also compares the formalization process with traditional proof techniques, considering both advantages such as absolute rigor and machine-checkable verification, and trade-offs such as verbosity, learning curve, and limited automation.
CDT is UTC-5. This Differential Geometry, PDE and Mathematical Physics seminar is available over zoom.
 | Wednesday
Apr. 15
4 PM
Math 011
|
| Applied Mathematics and Machine Learning
TBA
Yulong Ying
The Ohio State University, Department of Mathematics
|
TTU Math Circle Spring Flyer 6:30-7:30 PM Thursdays in the basement of Math, room 010
abstract 2 PM CDT (UTC-5)
Zoom link available from Dr. Brent Lindquist upon request.
