Lean Paris

Lean is a state-of-the-art theorem prover and programming language designed for interactive theorem proving, formal verification, and the development of reliable software and mathematics. It enables humans and machines to collaborate on building rigorous proofs and verified systems, and it has rapidly become one of the most influential platforms in the growing ecosystem of formal reasoning tools.

The Paris Lean Meetup welcomes anyone curious about the future of formal verification and the role that theorem proving may play in science, technology, and education. Our community brings together mathematicians, programmers, educators, researchers, students, engineers, and industry practitioners, as well as anyone interested in exploring how formal reasoning can transform the way we build knowledge and software.

Key themes we'll explore include:

• AI and automated reasoning, including new approaches to machine-assisted mathematics and theorem discovery
• formal verification of software, systems, and cryptographic protocols
• formalized mathematics and the rapidly growing mathlib ecosystem
• programming languages, type theory, and proof assistants
• education and new methods for teaching mathematics and logic

By bringing these communities together, we aim to create a space where ideas from research, industry, and open-source development can meet and evolve.

Each meetup session consists of one or two talks followed by informal social time, giving participants the opportunity to exchange ideas, discuss projects, and connect with others interested in Lean and formal methods.