Yuyuan Yuan
A Rustacean working in ZettaScale Technology. Developing Zenoh, an open-source protocol designed to enable efficient and scalable distributed systems for applications such as autonomous systems, drones, and robotics. Always exploring new technologies!
Intervention
Lean is an interactive theorem prover that is revolutionizing how mathematical proofs are written and verified. As an open-source project, Lean has fostered a growing community of mathematicians, logicians, and programmers who are collaboratively building a comprehensive library of formalized mathematics. This talk will introduce Lean’s core concepts, explore its underlying type theory, and demonstrate how it enables rigorous, computer-verified proofs. No prior experience with proof assistants is required.