Lean Together 2024

logic in computer science mathematical software Mathematics

Audience:	Researchers in the discipline
Conference dates:	09-Jan-2024 to 12-Jan-2024
Organizers:	David Thrane Christiansen, Robert Y. Lewis, Patrick Massot
	*contact for this listing

Upcoming talks

Past talks

Your time			Speaker	Title
Fri	Jan 12	18:30	Social hour	TBA
Fri	Jan 12	18:00	Joe Hendrix	Standard Library 2024
Fri	Jan 12	17:30	Jad Elkhaleq Ghalayini	Formalizing refinement types in Lean
Fri	Jan 12	17:15	Coffee break	TBA
Fri	Jan 12	16:45	Ramon Fernández Mir	CvxLean: modeling convex optimization problems in Lean
Fri	Jan 12	16:15	María Inés de Frutos Fernández	Formalizing local fields in Lean
Fri	Jan 12	16:00	Coffee break	TBA
Fri	Jan 12	15:00	Leonardo de Moura	Lean FRO meeting
Thu	Jan 11	17:00	Social hour	TBA
Thu	Jan 11	16:30	Wrenna Robson	Permutations on bitvectors: an inductive perspective
Thu	Jan 11	16:00	Kaiyu Yang	Towards Large Language Models as Copilots for Theorem Proving in Lean
Thu	Jan 11	15:45	Coffee break	TBA
Thu	Jan 11	15:15	David Thrane Christiansen	Documentation as a DSL
Thu	Jan 11	14:45	Evgenia Karunus, Anton Kovsharov	Visualising a proof: introducing Paperproof
Thu	Jan 11	14:15	Leonidas Lampropoulos	QuickChick: Property-Based Testing in Coq
Thu	Jan 11	14:00	Coffee break	TBA
Thu	Jan 11	13:30	Josh Clune	Duper: A Higher-Order Proof Producing Superposition Theorem Prover
Thu	Jan 11	13:00	Yicheng Qian	Auto: An Interface Between Lean and Automated Theorem Provers
Thu	Jan 11	12:30	Andrew Yang	Fermat’s last theorem for regular primes - Case II
Wed	Jan 10	20:30	Social hour	TBA
Wed	Jan 10	20:00	Jireh Loreaux	Operator algebras in Mathlib: status and roadmap
Wed	Jan 10	19:30	Ashvni Narayanan	p-adic L-functions in Lean
Wed	Jan 10	19:15	Coffee break	TBA
Wed	Jan 10	18:45	Mac Malone	How Reservoir Boosts Your Lean Packages
Wed	Jan 10	18:15	Sophie Morel	Formalizing Grassmannians in Lean
Wed	Jan 10	17:45	Alex Best	Leaff: a Lean library diff tool
Wed	Jan 10	17:30	Coffee break	TBA
Wed	Jan 10	17:00	Bhavik Mehta	Formalisation of combinatorics
Wed	Jan 10	16:30	Sorawee Porncharoenwase	A Pretty Expressive Printer
Wed	Jan 10	16:00	Joël Riou	Overview of homology in mathlib
Tue	Jan 09	18:15	Social hour	TBA
Tue	Jan 09	17:15	Emina Torlak	Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Tue	Jan 09	17:00	Coffee break	TBA
Tue	Jan 09	16:30	Dagur Ásgeirsson	Condensed mathematics in Mathlib
Tue	Jan 09	16:00	Tomáš Skřivan	Automatic differentiation in Lean
Tue	Jan 09	15:30	Nirvana Coppola	Formalization of class numbers computations and Mordell equations
Tue	Jan 09	15:15	Coffee break	TBA
Tue	Jan 09	14:45	Rémy Degenne	Probability in the formalization of the Polynomial Freiman Ruzsa conjecture
Tue	Jan 09	14:15	Sebastian Ullrich	Are We Fast Yet
Tue	Jan 09	14:00	Patrick Massot	Welcome

Embed this schedule

Export series to