09/08/2025 –, RB105
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.
Anyone in COSCUP. No prior experience with proof assistants is required.
Niveau de difficulté:初學者
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!